|   | 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 412 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | 
| 3 | anim12dan.2 | . . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜏) | |
| 4 | 3 | ex 412 | . . 3 ⊢ (𝜑 → (𝜃 → 𝜏)) | 
| 5 | 2, 4 | anim12d 609 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏))) | 
| 6 | 5 | imp 406 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → (𝜒 ∧ 𝜏)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 | 
| 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 207 df-an 396 | 
| This theorem is referenced by: 2f1fvneq 7281 isocnv 7351 isocnv3 7353 f1oiso2 7373 xpexr2 7942 f1o2ndf1 8148 fnwelem 8157 omword 8609 oeword 8629 swoso 8780 xpf1o 9180 zorn2lem6 10542 ltapr 11086 ltord1 11790 pc11 16919 imasaddfnlem 17574 imasaddflem 17576 pslem 18618 mgmhmpropd 18712 mhmpropd 18806 frmdsssubm 18875 ghmsub 19243 gasubg 19321 invrpropd 20419 znfld 21580 cygznlem3 21589 mplcoe5lem 22058 evlseu 22108 cpmatmcl 22726 tgclb 22978 innei 23134 txcn 23635 txflf 24015 qustgplem 24130 clmsub4 25140 cfilresi 25330 volcn 25642 itg1addlem4 25735 dvlip 26033 plymullem1 26254 lgsdir2 27375 lgsdchr 27400 brbtwn2 28921 axcontlem7 28986 frgrncvvdeqlem8 30326 nvaddsub4 30677 hhcno 31924 hhcnf 31925 unopf1o 31936 counop 31941 mndlactf1o 33036 mndractf1o 33037 afsval 34687 ontopbas 36430 onsuct0 36443 heicant 37663 ftc1anclem6 37706 equivbnd2 37800 ismtybndlem 37814 ismrer1 37846 iccbnd 37848 ghomco 37899 rngohomco 37982 rngoisocnv 37989 rngoisoco 37990 idlsubcl 38031 xihopellsmN 41257 dihopellsm 41258 f1o2d2 42274 dvconstbi 44358 ovolval5lem3 46674 imasetpreimafvbijlemf1 47396 fargshiftf1 47433 elpglem1 49285 | 
| Copyright terms: Public domain | W3C validator |