MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anim12dan Structured version   Visualization version   GIF version

Theorem anim12dan 618
Description: Conjoin antecedents and consequents in a deduction. (Contributed by Mario Carneiro, 12-May-2014.)
Hypotheses
Ref Expression
anim12dan.1 ((𝜑𝜓) → 𝜒)
anim12dan.2 ((𝜑𝜃) → 𝜏)
Assertion
Ref Expression
anim12dan ((𝜑 ∧ (𝜓𝜃)) → (𝜒𝜏))

Proof of Theorem anim12dan
StepHypRef Expression
1 anim12dan.1 . . . 4 ((𝜑𝜓) → 𝜒)
21ex 413 . . 3 (𝜑 → (𝜓𝜒))
3 anim12dan.2 . . . 4 ((𝜑𝜃) → 𝜏)
43ex 413 . . 3 (𝜑 → (𝜃𝜏))
52, 4anim12d 608 . 2 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
65imp 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  7012  isocnv  7075  isocnv3  7077  f1oiso2  7097  xpexr2  7612  f1o2ndf1  7809  fnwelem  7816  omword  8186  oeword  8206  swoso  8312  xpf1o  8668  zorn2lem6  9912  ltapr  10456  ltord1  11155  pc11  16206  imasaddfnlem  16791  imasaddflem  16793  pslem  17806  mhmpropd  17950  frmdsssubm  18009  ghmsub  18296  gasubg  18362  invrpropd  19368  mplcoe5lem  20167  evlseu  20215  znfld  20626  cygznlem3  20635  cpmatmcl  21246  tgclb  21497  innei  21652  txcn  22153  txflf  22533  qustgplem  22647  clmsub4  23628  cfilresi  23816  volcn  24125  itg1addlem4  24218  dvlip  24508  plymullem1  24722  lgsdir2  25823  lgsdchr  25848  brbtwn2  26608  axcontlem7  26673  frgrncvvdeqlem8  28002  nvaddsub4  28351  hhcno  29598  hhcnf  29599  unopf1o  29610  counop  29615  afsval  31831  ontopbas  33663  onsuct0  33676  heicant  34797  ftc1anclem6  34842  anim12da  34858  equivbnd2  34941  ismtybndlem  34955  ismrer1  34987  iccbnd  34989  xihopellsmN  38260  dihopellsm  38261  dvconstbi  40534  fargshiftf1  43436  mgmhmpropd  43887  elpglem1  44648
  Copyright terms: Public domain W3C validator