![]() |
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 449 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | jaoian.2 | . . . 4 ⊢ ((𝜃 ∧ 𝜓) → 𝜒) | |
4 | 3 | ex 449 | . . 3 ⊢ (𝜃 → (𝜓 → 𝜒)) |
5 | 2, 4 | jaoi 393 | . 2 ⊢ ((𝜑 ∨ 𝜃) → (𝜓 → 𝜒)) |
6 | 5 | imp 444 | 1 ⊢ (((𝜑 ∨ 𝜃) ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 382 ∧ wa 383 |
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 197 df-or 384 df-an 385 |
This theorem is referenced by: ccase 1024 preq12nebg 4541 opthprneg 4543 elpreqpr 4545 tpres 6628 xaddnemnf 12258 xaddnepnf 12259 faclbnd 13269 faclbnd3 13271 faclbnd4lem1 13272 znf1o 20100 degltlem1 24029 ipasslem3 27995 padct 29804 fz1nntr 29868 xrge0iifhom 30290 fzsplit1nn0 37817 |
Copyright terms: Public domain | W3C validator |