![]() |
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 499 | 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 586 anim1d 587 anim2d 588 prth 594 im2anan9 898 anim12dan 900 3anim123d 1446 mo3 2536 2euswap 2577 ssunsn2 4391 disjiun 4672 soss 5082 wess 5130 frinxp 5218 trin2 5554 xp11 5604 ordtri3OLD 5798 oneqmini 5814 funss 5945 fun 6104 fvcofneq 6407 dff13 6552 f1cofveqaeq 6555 f1eqcocnv 6596 isores3 6625 isosolem 6637 isowe2 6640 ordom 7116 f1oweALT 7194 f1o2ndf1 7330 tposfn2 7419 tposf1o2 7423 wfrlem4 7463 smo11 7506 tz7.48lem 7581 om00 7700 omsmo 7779 ixpfi2 8305 elfiun 8377 supmo 8399 infmo 8442 alephord 8936 cardaleph 8950 dfac5 8989 fin1a2lem9 9268 axdc3lem2 9311 zorn2lem6 9361 grudomon 9677 indpi 9767 genpnmax 9867 reclem3pr 9909 reclem4pr 9910 suplem1pr 9912 supsrlem 9970 dedekind 10238 lemul12b 10918 fimaxre 11006 lbreu 11011 supadd 11029 supmullem2 11032 cju 11054 nnind 11076 uz11 11748 xrre2 12039 qbtwnre 12068 xrsupexmnf 12173 xrinfmexpnf 12174 ico0 12259 ioc0 12260 ssfzoulel 12602 ishashinf 13285 swrdccatin2 13533 coss12d 13757 sqrlem6 14032 o1lo1 14312 ruclem9 15011 isprm3 15443 eulerthlem2 15534 prmdiveq 15538 ramub2 15765 cictr 16512 joinfval 17048 meetfval 17062 clatl 17163 lubun 17170 ipodrsima 17212 dirtr 17283 mulgpropd 17631 dprdss 18474 subrgdvds 18842 dmatsubcl 20352 scmatcrng 20375 epttop 20861 cnpresti 21140 cnprest 21141 lmmo 21232 1stcrest 21304 lly1stc 21347 txcnp 21471 addcnlem 22714 clmvscom 22936 caussi 23141 bcthlem5 23171 ovollb2lem 23302 voliunlem1 23364 ioombl1lem4 23375 rolle 23798 c1lip1 23805 c1lip3 23807 ulmval 24179 sqf11 24910 fsumvma 24983 dchrelbas3 25008 acopy 25769 brbtwn2 25830 axeuclidlem 25887 axcontlem9 25897 axcontlem10 25898 umgrvad2edg 26150 upgrwlkdvdelem 26688 usgr2wlkneq 26708 2wlkdlem6 26896 umgr2adedgwlklem 26909 umgr2adedgspth 26913 2pthfrgrrn2 27263 frgrnbnb 27273 fusgr2wsp2nb 27314 nmcvcn 27678 sspmval 27716 sspimsval 27721 sspph 27838 shsubcl 28205 shorth 28282 5oalem6 28646 strlem1 29237 atexch 29368 cdj3i 29428 xrofsup 29661 nnindf 29693 cnre2csqima 30085 erdszelem9 31307 erdsze2lem2 31312 ss2mcls 31591 funpsstri 31789 dfon2lem4 31815 dfon2 31821 trpredrec 31862 frmin 31867 wsuclem 31895 frrlem4 31908 nocvxminlem 32018 nocvxmin 32019 conway 32035 elfuns 32147 btwnswapid 32249 ifscgr 32276 hilbert1.2 32387 elicc3 32436 tailfb 32497 wl-mo3t 33488 ltflcei 33527 tan2h 33531 mblfinlem3 33578 fzmul 33667 metf1o 33681 ismtycnv 33731 ismtyres 33737 crngohomfo 33935 cossss 34320 hlhgt2 34993 hl2at 35009 2llnjN 35171 2lplnj 35224 linepsubN 35356 cdlemg33b0 36306 dvh3dim3N 37055 mapdh9a 37396 iocinico 38114 clcnvlem 38247 pm11.59 38908 afvres 41573 rhmsscrnghm 42351 ply1mulgsumlem1 42499 fldivexpfllog2 42684 |
Copyright terms: Public domain | W3C validator |