![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > anim12d | Structured version Visualization version GIF version |
Description: Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.) |
Ref | Expression |
---|---|
anim12d.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
anim12d.2 | ⊢ (𝜑 → (𝜃 → 𝜏)) |
Ref | Expression |
---|---|
anim12d | ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anim12d.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | anim12d.2 | . 2 ⊢ (𝜑 → (𝜃 → 𝜏)) | |
3 | idd 24 | . 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜏) → (𝜒 ∧ 𝜏))) | |
4 | 1, 2, 3 | syl2and 501 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 385 |
This theorem is referenced by: anim12d1 588 anim1d 589 anim2d 590 prth 596 im2anan9 916 anim12dan 918 3anim123d 1555 mo3 2645 2euswap 2686 ssunsn2 4504 prel12g 4544 disjiun 4792 soss 5205 wess 5253 frinxp 5341 trin2 5677 xp11 5727 ordtri3OLD 5921 oneqmini 5937 funss 6068 fun 6227 fvcofneq 6530 dff13 6675 f1cofveqaeq 6678 f1eqcocnv 6719 isores3 6748 isosolem 6760 isowe2 6763 ordom 7239 f1oweALT 7317 f1o2ndf1 7453 tposfn2 7543 tposf1o2 7547 wfrlem4 7587 smo11 7630 tz7.48lem 7705 om00 7824 omsmo 7903 ixpfi2 8429 elfiun 8501 supmo 8523 infmo 8566 alephord 9088 cardaleph 9102 dfac5 9141 fin1a2lem9 9422 axdc3lem2 9465 zorn2lem6 9515 grudomon 9831 indpi 9921 genpnmax 10021 reclem3pr 10063 reclem4pr 10064 suplem1pr 10066 supsrlem 10124 dedekind 10392 lemul12b 11072 fimaxre 11160 lbreu 11165 supadd 11183 supmullem2 11186 cju 11208 nnind 11230 uz11 11902 xrre2 12194 qbtwnre 12223 xrsupexmnf 12328 xrinfmexpnf 12329 ico0 12414 ioc0 12415 ssfzoulel 12756 ishashinf 13439 swrdccatin2 13687 coss12d 13912 sqrlem6 14187 o1lo1 14467 ruclem9 15166 isprm3 15598 eulerthlem2 15689 prmdiveq 15693 ramub2 15920 cictr 16666 joinfval 17202 meetfval 17216 clatl 17317 lubun 17324 ipodrsima 17366 dirtr 17437 mulgpropd 17785 dprdss 18628 subrgdvds 18996 dmatsubcl 20506 scmatcrng 20529 epttop 21015 cnpresti 21294 cnprest 21295 lmmo 21386 1stcrest 21458 lly1stc 21501 txcnp 21625 addcnlem 22868 clmvscom 23090 caussi 23295 bcthlem5 23325 ovollb2lem 23456 voliunlem1 23518 ioombl1lem4 23529 rolle 23952 c1lip1 23959 c1lip3 23961 ulmval 24333 sqf11 25064 fsumvma 25137 dchrelbas3 25162 acopy 25923 brbtwn2 25984 axeuclidlem 26041 axcontlem9 26051 axcontlem10 26052 umgrvad2edg 26304 upgrwlkdvdelem 26842 usgr2wlkneq 26862 2wlkdlem6 27051 umgr2adedgwlklem 27064 umgr2adedgspth 27068 2pthfrgrrn2 27437 frgrnbnb 27447 fusgr2wsp2nb 27488 nmcvcn 27859 sspmval 27897 sspimsval 27902 sspph 28019 shsubcl 28386 shorth 28463 5oalem6 28827 strlem1 29418 atexch 29549 cdj3i 29609 xrofsup 29842 nnindf 29874 cnre2csqima 30266 erdszelem9 31488 erdsze2lem2 31493 ss2mcls 31772 funpsstri 31970 dfon2lem4 31996 dfon2 32002 trpredrec 32043 frmin 32048 wsuclem 32076 frrlem4 32089 nocvxminlem 32199 nocvxmin 32200 conway 32216 elfuns 32328 btwnswapid 32430 ifscgr 32457 hilbert1.2 32568 elicc3 32617 tailfb 32678 wl-mo3t 33671 ltflcei 33710 tan2h 33714 mblfinlem3 33761 fzmul 33850 metf1o 33864 ismtycnv 33914 ismtyres 33920 crngohomfo 34118 cossss 34503 hlhgt2 35178 hl2at 35194 2llnjN 35356 2lplnj 35409 linepsubN 35541 cdlemg33b0 36491 dvh3dim3N 37240 mapdh9a 37581 iocinico 38299 clcnvlem 38432 pm11.59 39093 afvres 41758 rhmsscrnghm 42536 ply1mulgsumlem1 42684 fldivexpfllog2 42869 |
Copyright terms: Public domain | W3C validator |