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

Theorem 3anim1i 1240
Description: Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 16-Aug-2009.)
Hypothesis
Ref Expression
3animi.1 (𝜑𝜓)
Assertion
Ref Expression
3anim1i ((𝜑𝜒𝜃) → (𝜓𝜒𝜃))

Proof of Theorem 3anim1i
StepHypRef Expression
1 3animi.1 . 2 (𝜑𝜓)
2 id 22 . 2 (𝜒𝜒)
3 id 22 . 2 (𝜃𝜃)
41, 2, 33anim123i 1239 1 ((𝜑𝜒𝜃) → (𝜓𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  syl3an1  1350  syl3anl1  1365  syl3anr1  1369  fnsuppres  7182  elfiun  8192  elioc2  12059  elico2  12060  elicc2  12061  dvdsleabs2  14814  mulgnndir  17334  mulgnnass  17341  trliswlk  25831  isspthonpth  25876  usg2wotspth  26173  cm2j  27665  bnj544  30020  btwnconn1lem4  31169  relowlssretop  32186  dalem53  33828  dalem54  33829  paddasslem14  33936  mzpcong  36356  spthonpthon  40955  uhgr1wlkspth  40959  usgr2wlkspth  40963  upgriseupth  41373
  Copyright terms: Public domain W3C validator