![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > jao1i | Structured version Visualization version GIF version |
Description: Add a disjunct in the antecedent of an implication. (Contributed by Rodolfo Medina, 24-Sep-2010.) |
Ref | Expression |
---|---|
jao1i.1 | ⊢ (𝜓 → (𝜒 → 𝜑)) |
Ref | Expression |
---|---|
jao1i | ⊢ ((𝜑 ∨ 𝜓) → (𝜒 → 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1 6 | . 2 ⊢ (𝜑 → (𝜒 → 𝜑)) | |
2 | jao1i.1 | . 2 ⊢ (𝜓 → (𝜒 → 𝜑)) | |
3 | 1, 2 | jaoi 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 |