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

Theorem 3jaod 1238
Description: Disjunction of 3 antecedents (deduction). (Contributed by NM, 14-Oct-2005.)
Hypotheses
Ref Expression
3jaod.1 (𝜑 → (𝜓𝜒))
3jaod.2 (𝜑 → (𝜃𝜒))
3jaod.3 (𝜑 → (𝜏𝜒))
Assertion
Ref Expression
3jaod (𝜑 → ((𝜓𝜃𝜏) → 𝜒))

Proof of Theorem 3jaod
StepHypRef Expression
1 3jaod.1 . 2 (𝜑 → (𝜓𝜒))
2 3jaod.2 . 2 (𝜑 → (𝜃𝜒))
3 3jaod.3 . 2 (𝜑 → (𝜏𝜒))
4 3jao 1235 . 2 (((𝜓𝜒) ∧ (𝜃𝜒) ∧ (𝜏𝜒)) → ((𝜓𝜃𝜏) → 𝜒))
51, 2, 3, 4syl3anc 1172 1 (𝜑 → ((𝜓𝜃𝜏) → 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  w3o 921
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663
This theorem depends on definitions:  df-bi 115  df-3or 923  df-3an 924
This theorem is referenced by:  3jaodan  1240  3jaao  1242  issod  4120  nnawordex  6239  addlocprlem  7038  nqprloc  7048  ltexprlemrl  7113  aptiprleml  7142  aptiprlemu  7143  elnn0z  8696  zaddcl  8723  zletric  8727  zlelttric  8728  zltnle  8729  zdceq  8755  zdcle  8756  zdclt  8757  nn01to3  9034  fzdcel  9386  qletric  9583  qlelttric  9584  qltnle  9585  qdceq  9586  frec2uzlt2d  9739
  Copyright terms: Public domain W3C validator