Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > anim12dan | Structured version Visualization version GIF version |
Description: Conjoin antecedents and consequents in a deduction. (Contributed by Jeff Madsen, 16-Jun-2011.) |
Ref | Expression |
---|---|
anim12dan.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
anim12dan.2 | ⊢ ((𝜑 ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
anim12dan | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → (𝜒 ∧ 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anim12dan.1 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | 1 | ex 413 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | anim12dan.2 | . . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜏) | |
4 | 3 | ex 413 | . . 3 ⊢ (𝜑 → (𝜃 → 𝜏)) |
5 | 2, 4 | anim12d 608 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏))) |
6 | 5 | imp 407 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → (𝜒 ∧ 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: 2f1fvneq 7009 isocnv 7072 isocnv3 7074 f1oiso2 7094 xpexr2 7613 f1o2ndf1 7807 fnwelem 7814 omword 8185 oeword 8205 swoso 8311 xpf1o 8667 zorn2lem6 9911 ltapr 10455 ltord1 11154 pc11 16204 imasaddfnlem 16789 imasaddflem 16791 pslem 17804 mhmpropd 17950 frmdsssubm 18014 ghmsub 18304 gasubg 18370 invrpropd 19377 mplcoe5lem 20176 evlseu 20224 znfld 20635 cygznlem3 20644 cpmatmcl 21255 tgclb 21506 innei 21661 txcn 22162 txflf 22542 qustgplem 22656 clmsub4 23637 cfilresi 23825 volcn 24134 itg1addlem4 24227 dvlip 24517 plymullem1 24731 lgsdir2 25833 lgsdchr 25858 brbtwn2 26618 axcontlem7 26683 frgrncvvdeqlem8 28012 nvaddsub4 28361 hhcno 29608 hhcnf 29609 unopf1o 29620 counop 29625 afsval 31841 ontopbas 33673 onsuct0 33686 heicant 34808 ftc1anclem6 34853 equivbnd2 34951 ismtybndlem 34965 ismrer1 34997 iccbnd 34999 ghomco 35050 rngohomco 35133 rngoisocnv 35140 rngoisoco 35141 idlsubcl 35182 xihopellsmN 38270 dihopellsm 38271 dvconstbi 40543 imasetpreimafvbijlemf1 43441 fargshiftf1 43478 mgmhmpropd 43929 elpglem1 44741 |
Copyright terms: Public domain | W3C validator |