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

Theorem jao1i 858
Description: Add a disjunct in the antecedent of an implication. (Contributed by Rodolfo Medina, 24-Sep-2010.)
Hypothesis
Ref Expression
jao1i.1 (𝜓 → (𝜒𝜑))
Assertion
Ref Expression
jao1i ((𝜑𝜓) → (𝜒𝜑))

Proof of Theorem jao1i
StepHypRef Expression
1 ax-1 6 . 2 (𝜑 → (𝜒𝜑))
2 jao1i.1 . 2 (𝜓 → (𝜒𝜑))
31, 2jaoi 857 1 ((𝜑𝜓) → (𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 847
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-or 848
This theorem is referenced by:  pm2.64  942  pm2.82  976  sorpssint  7521  preleqg  9230  ltlen  10933  elnnnn0b  12134  znnn0nn  12289  scshwfzeqfzo  14391  nn0enne  15938  dvdsprmpweqnn  16438  dvdsprmpweqle  16439  prmirred  20461  pmatcollpw3fi1  21685  2lgsoddprmlem3  26295  prtlem14  36625
  Copyright terms: Public domain W3C validator