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

Theorem 3anim1i 1149
 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 1148 1 ((𝜑𝜒𝜃) → (𝜓𝜒𝜃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  syl3an1  1160  syl3anl1  1409  syl3anr1  1413  fnsuppres  7832  elfiun  8870  elioc2  12778  elico2  12779  elicc2  12780  dvdsleabs2  15641  cphipval  23826  spthonpthon  27519  uhgrwkspth  27523  usgr2wlkspth  27527  upgriseupth  27971  cm2j  29382  bnj544  32174  btwnconn1lem4  33559  relowlssretop  34664  dalem53  36903  dalem54  36904  paddasslem14  37011  mzpcong  39720  itscnhlc0xyqsol  44986
 Copyright terms: Public domain W3C validator