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

Theorem 3jaod 1304
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 1301 . 2 (((𝜓𝜒) ∧ (𝜃𝜒) ∧ (𝜏𝜒)) → ((𝜓𝜃𝜏) → 𝜒))
51, 2, 3, 4syl3anc 1238 1 (𝜑 → ((𝜓𝜃𝜏) → 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  w3o 977
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:  3jaodan  1306  3jaao  1308  issod  4319  nnawordex  6529  exmidontri2or  7241  addlocprlem  7533  nqprloc  7543  ltexprlemrl  7608  aptiprleml  7637  aptiprlemu  7638  elnn0z  9265  zaddcl  9292  zletric  9296  zlelttric  9297  zltnle  9298  zdceq  9327  zdcle  9328  zdclt  9329  nn01to3  9616  xposdif  9881  fzdcel  10039  qletric  10243  qlelttric  10244  qltnle  10245  qdceq  10246  frec2uzlt2d  10403  triap  14713  tridceq  14740
  Copyright terms: Public domain W3C validator