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

Theorem jca32 310
Description: Join three consequents. (Contributed by FL, 1-Aug-2009.)
Hypotheses
Ref Expression
jca31.1 (𝜑𝜓)
jca31.2 (𝜑𝜒)
jca31.3 (𝜑𝜃)
Assertion
Ref Expression
jca32 (𝜑 → (𝜓 ∧ (𝜒𝜃)))

Proof of Theorem jca32
StepHypRef Expression
1 jca31.1 . 2 (𝜑𝜓)
2 jca31.2 . . 3 (𝜑𝜒)
3 jca31.3 . . 3 (𝜑𝜃)
42, 3jca 306 . 2 (𝜑 → (𝜒𝜃))
51, 4jca 306 1 (𝜑 → (𝜓 ∧ (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108
This theorem is referenced by:  syl12anc  1236  euan  2082  imadiflem  5294  supelti  6998  ltexnqq  7404  enq0sym  7428  enq0tr  7430  addclpr  7533  mulclpr  7568  ltexprlemopl  7597  ltexprlemlol  7598  ltexprlemopu  7599  ltexprlemupu  7600  suplocexprlemloc  7717  lemul12a  8815  fzass4  10057  elfz1b  10085  4fvwrd4  10135  leexp1a  10570  sqrt0rlem  11005  reumodprminv  12245  uptx  13645  distspace  13706  xmetxpbl  13879  bj-charfundc  14420
  Copyright terms: Public domain W3C validator