| 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 412 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
| 3 | jaoian.2 | . . . 4 ⊢ ((𝜃 ∧ 𝜓) → 𝜒) | |
| 4 | 3 | ex 412 | . . 3 ⊢ (𝜃 → (𝜓 → 𝜒)) |
| 5 | 2, 4 | jaoi 858 | . 2 ⊢ ((𝜑 ∨ 𝜃) → (𝜓 → 𝜒)) |
| 6 | 5 | imp 406 | 1 ⊢ (((𝜑 ∨ 𝜃) ∧ 𝜓) → 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∨ 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-an 396 df-or 849 |
| This theorem is referenced by: ccase 1038 preq12nebg 4863 opthprneg 4865 elpreqpr 4867 tpres 7221 xaddnemnf 13278 xaddnepnf 13279 faclbnd 14329 faclbnd3 14331 faclbnd4lem1 14332 znf1o 21570 degltlem1 26111 ipasslem3 30852 padct 32731 fz1nntr 32806 xrge0iifhom 33936 bj-ideqg1ALT 37166 nn0addcom 42480 nn0mulcom 42484 fzsplit1nn0 42765 f1mo 48762 |
| Copyright terms: Public domain | W3C validator |