Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > jaoian | Structured version Visualization version GIF version |
Description: Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005.) |
Ref | Expression |
---|---|
jaoian.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
jaoian.2 | ⊢ ((𝜃 ∧ 𝜓) → 𝜒) |
Ref | Expression |
---|---|
jaoian | ⊢ (((𝜑 ∨ 𝜃) ∧ 𝜓) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jaoian.1 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | 1 | ex 416 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | jaoian.2 | . . . 4 ⊢ ((𝜃 ∧ 𝜓) → 𝜒) | |
4 | 3 | ex 416 | . . 3 ⊢ (𝜃 → (𝜓 → 𝜒)) |
5 | 2, 4 | jaoi 857 | . 2 ⊢ ((𝜑 ∨ 𝜃) → (𝜓 → 𝜒)) |
6 | 5 | imp 410 | 1 ⊢ (((𝜑 ∨ 𝜃) ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∨ 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 210 df-an 400 df-or 848 |
This theorem is referenced by: ccase 1038 preq12nebg 4773 opthprneg 4775 elpreqpr 4777 tpres 7016 xaddnemnf 12826 xaddnepnf 12827 faclbnd 13856 faclbnd3 13858 faclbnd4lem1 13859 znf1o 20516 degltlem1 24970 ipasslem3 28914 padct 30774 fz1nntr 30845 xrge0iifhom 31601 bj-ideqg1ALT 35071 fzsplit1nn0 40279 f1mo 45853 |
Copyright terms: Public domain | W3C validator |