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

Theorem 3anim1i 1241
 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 1240 1 ((𝜑𝜒𝜃) → (𝜓𝜒𝜃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  syl3an1  1351  syl3anl1  1366  syl3anr1  1370  fnsuppres  7209  elfiun  8219  elioc2  12107  elico2  12108  elicc2  12109  dvdsleabs2  14872  mulgnndir  17392  mulgnnass  17399  cphipval  22850  trliswlk  26069  isspthonpth  26114  usg2wotspth  26411  cm2j  27863  bnj544  30218  btwnconn1lem4  31367  relowlssretop  32387  dalem53  34029  dalem54  34030  paddasslem14  34137  mzpcong  36557  spthonpthon  40957  uhgr1wlkspth  40961  usgr2wlkspth  40965  upgriseupth  41375
 Copyright terms: Public domain W3C validator