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

Theorem 3anim1i 1246
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 1245 1 ((𝜑𝜒𝜃) → (𝜓𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  syl3an1  1356  syl3anl1  1371  syl3anr1  1375  fnsuppres  7282  elfiun  8296  elioc2  12194  elico2  12195  elicc2  12196  dvdsleabs2  14977  mulgnndir  17509  mulgnnass  17516  cphipval  22982  spthonpthon  26550  uhgrwkspth  26554  usgr2wlkspth  26558  upgriseupth  26967  cm2j  28367  bnj544  30725  btwnconn1lem4  31892  relowlssretop  32882  dalem53  34530  dalem54  34531  paddasslem14  34638  mzpcong  37058
  Copyright terms: Public domain W3C validator