Metamath Proof Explorer
Description: Inference separating a disjunct of an antecedent. (Contributed by Alexander van der Vekens, 25-May-2018)
|
|
Ref |
Expression |
|
Hypotheses |
jaoi3.1 |
⊢ ( 𝜑 → 𝜓 ) |
|
|
jaoi3.2 |
⊢ ( ( ¬ 𝜑 ∧ 𝜒 ) → 𝜓 ) |
|
Assertion |
jaoi3 |
⊢ ( ( 𝜑 ∨ 𝜒 ) → 𝜓 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
jaoi3.1 |
⊢ ( 𝜑 → 𝜓 ) |
2 |
|
jaoi3.2 |
⊢ ( ( ¬ 𝜑 ∧ 𝜒 ) → 𝜓 ) |
3 |
1 2
|
jaoi |
⊢ ( ( 𝜑 ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) → 𝜓 ) |
4 |
3
|
jaoi2 |
⊢ ( ( 𝜑 ∨ 𝜒 ) → 𝜓 ) |