ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3jaoi GIF version

Theorem 3jaoi 1303
Description: Disjunction of 3 antecedents (inference). (Contributed by NM, 12-Sep-1995.)
Hypotheses
Ref Expression
3jaoi.1 (𝜑𝜓)
3jaoi.2 (𝜒𝜓)
3jaoi.3 (𝜃𝜓)
Assertion
Ref Expression
3jaoi ((𝜑𝜒𝜃) → 𝜓)

Proof of Theorem 3jaoi
StepHypRef Expression
1 3jaoi.1 . . 3 (𝜑𝜓)
2 3jaoi.2 . . 3 (𝜒𝜓)
3 3jaoi.3 . . 3 (𝜃𝜓)
41, 2, 33pm3.2i 1175 . 2 ((𝜑𝜓) ∧ (𝜒𝜓) ∧ (𝜃𝜓))
5 3jao 1301 . 2 (((𝜑𝜓) ∧ (𝜒𝜓) ∧ (𝜃𝜓)) → ((𝜑𝜒𝜃) → 𝜓))
64, 5ax-mp 5 1 ((𝜑𝜒𝜃) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  w3o 977  w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709
This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980
This theorem is referenced by:  3jaoian  1305  3ianorr  1309  acexmidlem1  5864  nndceq  6493  nndcel  6494  znegcl  9260  xrltnr  9753  nltpnft  9788  ngtmnft  9791  xrrebnd  9793  xnegcl  9806  xnegneg  9807  xltnegi  9809  xrpnfdc  9816  xrmnfdc  9817  xnegid  9833  xaddid1  9836  xposdif  9856  prm23lt5  12233  zabsle1  14033
  Copyright terms: Public domain W3C validator