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

Theorem jao1i 852
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 851 1 ((𝜑𝜓) → (𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 841
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 842
This theorem is referenced by:  pm2.64  935  pm2.82  969  sorpssint  7448  preleqg  9066  ltlen  10729  elnnnn0b  11929  znnn0nn  12082  scshwfzeqfzo  14176  nn0enne  15716  dvdsprmpweqnn  16209  dvdsprmpweqle  16210  prmirred  20570  pmatcollpw3fi1  21324  2lgsoddprmlem3  25917  prtlem14  35890
  Copyright terms: Public domain W3C validator