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

Theorem 3anim1i 1144
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 1143 1 ((𝜑𝜒𝜃) → (𝜓𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  syl3an1  1155  syl3anl1  1404  syl3anr1  1408  fnsuppres  7846  elfiun  8882  elioc2  12787  elico2  12788  elicc2  12789  dvdsleabs2  15650  cphipval  23773  spthonpthon  27459  uhgrwkspth  27463  usgr2wlkspth  27467  upgriseupth  27913  cm2j  29324  bnj544  32065  btwnconn1lem4  33448  relowlssretop  34526  dalem53  36741  dalem54  36742  paddasslem14  36849  mzpcong  39447  itscnhlc0xyqsol  44680
  Copyright terms: Public domain W3C validator