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

Theorem 3jaod 1265
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 1262 . 2 (((𝜓𝜒) ∧ (𝜃𝜒) ∧ (𝜏𝜒)) → ((𝜓𝜃𝜏) → 𝜒))
51, 2, 3, 4syl3anc 1199 1 (𝜑 → ((𝜓𝜃𝜏) → 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  w3o 944
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 681
This theorem depends on definitions:  df-bi 116  df-3or 946  df-3an 947
This theorem is referenced by:  3jaodan  1267  3jaao  1269  issod  4209  nnawordex  6390  addlocprlem  7307  nqprloc  7317  ltexprlemrl  7382  aptiprleml  7411  aptiprlemu  7412  elnn0z  9018  zaddcl  9045  zletric  9049  zlelttric  9050  zltnle  9051  zdceq  9077  zdcle  9078  zdclt  9079  nn01to3  9358  xposdif  9605  fzdcel  9760  qletric  9961  qlelttric  9962  qltnle  9963  qdceq  9964  frec2uzlt2d  10117  triap  13047
  Copyright terms: Public domain W3C validator