![]() |
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 Mario Carneiro, 12-May-2014.) |
Ref | Expression |
---|---|
anim12dan.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
anim12dan.2 | ⊢ ((𝜑 ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
anim12dan | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → (𝜒 ∧ 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anim12dan.1 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | 1 | ex 449 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | anim12dan.2 | . . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜏) | |
4 | 3 | ex 449 | . . 3 ⊢ (𝜑 → (𝜃 → 𝜏)) |
5 | 2, 4 | anim12d 585 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏))) |
6 | 5 | imp 444 | 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: 2f1fvneq 6557 isocnv 6620 isocnv3 6622 f1oiso2 6642 xpexr2 7149 f1o2ndf1 7330 fnwelem 7337 omword 7695 oeword 7715 swoso 7820 xpf1o 8163 zorn2lem6 9361 ltapr 9905 ltord1 10592 pc11 15631 imasaddfnlem 16235 imasaddflem 16237 pslem 17253 mhmpropd 17388 frmdsssubm 17445 ghmsub 17715 gasubg 17781 invrpropd 18744 mplcoe5lem 19515 evlseu 19564 znfld 19957 cygznlem3 19966 cpmatmcl 20572 tgclb 20822 innei 20977 txcn 21477 txflf 21857 qustgplem 21971 clmsub4 22952 cfilresi 23139 volcn 23420 itg1addlem4 23511 dvlip 23801 plymullem1 24015 lgsdir2 25100 lgsdchr 25125 brbtwn2 25830 axcontlem7 25895 frgrncvvdeqlem8 27286 nvaddsub4 27640 hhcno 28891 hhcnf 28892 unopf1o 28903 counop 28908 afsval 30877 ontopbas 32552 onsuct0 32565 heicant 33574 ftc1anclem6 33620 anim12da 33636 equivbnd2 33721 ismtybndlem 33735 ismrer1 33767 iccbnd 33769 xihopellsmN 36860 dihopellsm 36861 dvconstbi 38850 fargshiftf1 41702 mgmhmpropd 42110 elpglem1 42782 |
Copyright terms: Public domain | W3C validator |