Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpjao3danOLD Structured version   Visualization version   GIF version

Theorem mpjao3danOLD 1429
 Description: Obsolete version of mpjao3dan 1428 as of 17-Apr-2024. (Contributed by Thierry Arnoux, 13-Apr-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
mpjao3dan.1 ((𝜑𝜓) → 𝜒)
mpjao3dan.2 ((𝜑𝜃) → 𝜒)
mpjao3dan.3 ((𝜑𝜏) → 𝜒)
mpjao3dan.4 (𝜑 → (𝜓𝜃𝜏))
Assertion
Ref Expression
mpjao3danOLD (𝜑𝜒)

Proof of Theorem mpjao3danOLD
StepHypRef Expression
1 mpjao3dan.1 . . 3 ((𝜑𝜓) → 𝜒)
2 mpjao3dan.2 . . 3 ((𝜑𝜃) → 𝜒)
31, 2jaodan 955 . 2 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
4 mpjao3dan.3 . 2 ((𝜑𝜏) → 𝜒)
5 mpjao3dan.4 . . 3 (𝜑 → (𝜓𝜃𝜏))
6 df-3or 1085 . . 3 ((𝜓𝜃𝜏) ↔ ((𝜓𝜃) ∨ 𝜏))
75, 6sylib 221 . 2 (𝜑 → ((𝜓𝜃) ∨ 𝜏))
83, 4, 7mpjaodan 956 1 (𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 844   ∨ w3o 1083 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 845  df-3or 1085 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator