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

Theorem jao1i 855
 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 854 1 ((𝜑𝜓) → (𝜒𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 844 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 845 This theorem is referenced by:  pm2.64  939  pm2.82  973  sorpssint  7441  preleqg  9064  ltlen  10732  elnnnn0b  11931  znnn0nn  12084  scshwfzeqfzo  14181  nn0enne  15720  dvdsprmpweqnn  16213  dvdsprmpweqle  16214  prmirred  20192  pmatcollpw3fi1  21400  2lgsoddprmlem3  26005  prtlem14  36186
 Copyright terms: Public domain W3C validator