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

Theorem 3jaod 1198
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 1195 . 2 (((ψχ) (θχ) (τχ)) → ((ψ θ τ) → χ))
51, 2, 3, 4syl3anc 1134 1 (φ → ((ψ θ τ) → χ))
Colors of variables: wff set class
Syntax hints:  wi 4   w3o 883
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629
This theorem depends on definitions:  df-bi 110  df-3or 885  df-3an 886
This theorem is referenced by:  3jaodan  1200  3jaao  1202  issod  4047  nnawordex  6037  addlocprlem  6517  nqprloc  6527  ltexprlemrl  6583  aptiprleml  6610  aptiprlemu  6611  elnn0z  8014  zaddcl  8041  zletric  8045  zlelttric  8046  zltnle  8047  zdceq  8072  zdcle  8073  zdclt  8074  nn01to3  8308  fzdcel  8654  frec2uzlt2d  8851
  Copyright terms: Public domain W3C validator