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 207  df-or 848
This theorem is referenced by:  pm2.64  943  pm2.82  977  sorpssint  7752  preleqg  9653  ltlen  11360  elnnnn0b  12568  znnn0nn  12727  scshwfzeqfzo  14862  nn0enne  16411  dvdsprmpweqnn  16919  dvdsprmpweqle  16920  prmirred  21503  pmatcollpw3fi1  22810  2lgsoddprmlem3  27473  sltlend  27831  prtlem14  38856
  Copyright terms: Public domain W3C validator