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

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

Proof of Theorem jca31
StepHypRef Expression
1 jca31.1 . . 3 (𝜑𝜓)
2 jca31.2 . . 3 (𝜑𝜒)
31, 2jca 306 . 2 (𝜑 → (𝜓𝜒))
4 jca31.3 . 2 (𝜑𝜃)
53, 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:  3jca  1179  syl21anbrc  1184  syl21anc  1248  f1oiso2  5844  exmidapne  7277  nnnq0lem1  7463  prmuloc  7583  suplocexprlemex  7739  prsrlem1  7759  apreap  8562  lemulge11  8841  elnnz  9281  supinfneg  9613  infsupneg  9614  leexp1a  10593  faclbnd6  10742  zfz1isolem1  10838  oddpwdclemdc  12191  ennnfonelemf1  12437  grpidinv2  12968  rhmopp  13487  dvdsrzring  13863  cncnp2m  14115  bj-charfun  14943
  Copyright terms: Public domain W3C validator