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

Theorem 3jaod 1283
 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 1280 . 2 (((𝜓𝜒) ∧ (𝜃𝜒) ∧ (𝜏𝜒)) → ((𝜓𝜃𝜏) → 𝜒))
51, 2, 3, 4syl3anc 1217 1 (𝜑 → ((𝜓𝜃𝜏) → 𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∨ w3o 962 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699 This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965 This theorem is referenced by:  3jaodan  1285  3jaao  1287  issod  4274  nnawordex  6464  exmidontri2or  7157  addlocprlem  7434  nqprloc  7444  ltexprlemrl  7509  aptiprleml  7538  aptiprlemu  7539  elnn0z  9159  zaddcl  9186  zletric  9190  zlelttric  9191  zltnle  9192  zdceq  9218  zdcle  9219  zdclt  9220  nn01to3  9504  xposdif  9764  fzdcel  9920  qletric  10121  qlelttric  10122  qltnle  10123  qdceq  10124  frec2uzlt2d  10281  triap  13541  tridceq  13568
 Copyright terms: Public domain W3C validator