![]() |
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 609 | . 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 206 df-an 397 |
This theorem is referenced by: 2f1fvneq 7206 isocnv 7274 isocnv3 7276 f1oiso2 7296 xpexr2 7855 f1o2ndf1 8053 fnwelem 8062 omword 8516 oeword 8536 swoso 8680 xpf1o 9082 zorn2lem6 10436 ltapr 10980 ltord1 11680 pc11 16751 imasaddfnlem 17409 imasaddflem 17411 pslem 18460 mhmpropd 18607 frmdsssubm 18670 ghmsub 19014 gasubg 19080 invrpropd 20125 znfld 20965 cygznlem3 20974 mplcoe5lem 21438 evlseu 21491 cpmatmcl 22066 tgclb 22318 innei 22474 txcn 22975 txflf 23355 qustgplem 23470 clmsub4 24467 cfilresi 24657 volcn 24968 itg1addlem4 25061 itg1addlem4OLD 25062 dvlip 25355 plymullem1 25573 lgsdir2 26676 lgsdchr 26701 brbtwn2 27852 axcontlem7 27917 frgrncvvdeqlem8 29248 nvaddsub4 29597 hhcno 30844 hhcnf 30845 unopf1o 30856 counop 30861 afsval 33275 ontopbas 34891 onsuct0 34904 heicant 36104 ftc1anclem6 36147 equivbnd2 36242 ismtybndlem 36256 ismrer1 36288 iccbnd 36290 ghomco 36341 rngohomco 36424 rngoisocnv 36431 rngoisoco 36432 idlsubcl 36473 xihopellsmN 39708 dihopellsm 39709 mhphf 40749 dvconstbi 42596 ovolval5lem3 44867 imasetpreimafvbijlemf1 45568 fargshiftf1 45605 mgmhmpropd 46051 elpglem1 47128 |
Copyright terms: Public domain | W3C validator |