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

Theorem 3jaod 1210
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 1207 . 2 (((𝜓𝜒) ∧ (𝜃𝜒) ∧ (𝜏𝜒)) → ((𝜓𝜃𝜏) → 𝜒))
51, 2, 3, 4syl3anc 1146 1 (𝜑 → ((𝜓𝜃𝜏) → 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  w3o 895
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640
This theorem depends on definitions:  df-bi 114  df-3or 897  df-3an 898
This theorem is referenced by:  3jaodan  1212  3jaao  1214  issod  4084  nnawordex  6132  addlocprlem  6691  nqprloc  6701  ltexprlemrl  6766  aptiprleml  6795  aptiprlemu  6796  elnn0z  8315  zaddcl  8342  zletric  8346  zlelttric  8347  zltnle  8348  zdceq  8374  zdcle  8375  zdclt  8376  nn01to3  8649  fzdcel  9006  qletric  9201  qlelttric  9202  qltnle  9203  qdceq  9204  frec2uzlt2d  9354
  Copyright terms: Public domain W3C validator