![]() |
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 855 | 1 ⊢ ((𝜑 ∨ 𝜓) → (𝜒 → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 845 |
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 206 df-or 846 |
This theorem is referenced by: pm2.64 939 pm2.82 973 sorpssint 7734 preleqg 9649 ltlen 11354 elnnnn0b 12560 znnn0nn 12717 scshwfzeqfzo 14828 nn0enne 16372 dvdsprmpweqnn 16880 dvdsprmpweqle 16881 prmirred 21458 pmatcollpw3fi1 22776 2lgsoddprmlem3 27438 sltlend 27796 prtlem14 38583 |
Copyright terms: Public domain | W3C validator |