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

Theorem anim12dan 918
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 449 . . 3 (𝜑 → (𝜓𝜒))
3 anim12dan.2 . . . 4 ((𝜑𝜃) → 𝜏)
43ex 449 . . 3 (𝜑 → (𝜃𝜏))
52, 4anim12d 587 . 2 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
65imp 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  6680  isocnv  6743  isocnv3  6745  f1oiso2  6765  xpexr2  7272  f1o2ndf1  7453  fnwelem  7460  omword  7819  oeword  7839  swoso  7944  xpf1o  8287  zorn2lem6  9515  ltapr  10059  ltord1  10746  pc11  15786  imasaddfnlem  16390  imasaddflem  16392  pslem  17407  mhmpropd  17542  frmdsssubm  17599  ghmsub  17869  gasubg  17935  invrpropd  18898  mplcoe5lem  19669  evlseu  19718  znfld  20111  cygznlem3  20120  cpmatmcl  20726  tgclb  20976  innei  21131  txcn  21631  txflf  22011  qustgplem  22125  clmsub4  23106  cfilresi  23293  volcn  23574  itg1addlem4  23665  dvlip  23955  plymullem1  24169  lgsdir2  25254  lgsdchr  25279  brbtwn2  25984  axcontlem7  26049  frgrncvvdeqlem8  27460  nvaddsub4  27821  hhcno  29072  hhcnf  29073  unopf1o  29084  counop  29089  afsval  31058  ontopbas  32733  onsuct0  32746  heicant  33757  ftc1anclem6  33803  anim12da  33819  equivbnd2  33904  ismtybndlem  33918  ismrer1  33950  iccbnd  33952  xihopellsmN  37045  dihopellsm  37046  dvconstbi  39035  fargshiftf1  41887  mgmhmpropd  42295  elpglem1  42967
  Copyright terms: Public domain W3C validator