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

Theorem jao1i 853
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 852 1 ((𝜑𝜓) → (𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 842
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-or 843
This theorem is referenced by:  pm2.64  936  pm2.82  970  sorpssint  7324  preleqg  8931  ltlen  10594  elnnnn0b  11795  znnn0nn  11948  scshwfzeqfzo  14028  nn0enne  15565  dvdsprmpweqnn  16054  dvdsprmpweqle  16055  prmirred  20328  pmatcollpw3fi1  21084  2lgsoddprmlem3  25676  prtlem14  35562
  Copyright terms: Public domain W3C validator