|   | 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 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 |