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

Theorem jao1i 859
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 858 1 ((𝜑𝜓) → (𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 848
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 207  df-or 849
This theorem is referenced by:  pm2.64  944  pm2.82  978  imadifssran  6171  sorpssint  7753  preleqg  9655  ltlen  11362  elnnnn0b  12570  znnn0nn  12729  scshwfzeqfzo  14865  nn0enne  16414  dvdsprmpweqnn  16923  dvdsprmpweqle  16924  prmirred  21485  pmatcollpw3fi1  22794  2lgsoddprmlem3  27458  sltlend  27816  prtlem14  38875
  Copyright terms: Public domain W3C validator