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

Theorem 3anim123i 1186
Description: Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994.)
Hypotheses
Ref Expression
3anim123i.1 (𝜑𝜓)
3anim123i.2 (𝜒𝜃)
3anim123i.3 (𝜏𝜂)
Assertion
Ref Expression
3anim123i ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))

Proof of Theorem 3anim123i
StepHypRef Expression
1 3anim123i.1 . . 3 (𝜑𝜓)
213ad2ant1 1020 . 2 ((𝜑𝜒𝜏) → 𝜓)
3 3anim123i.2 . . 3 (𝜒𝜃)
433ad2ant2 1021 . 2 ((𝜑𝜒𝜏) → 𝜃)
5 3anim123i.3 . . 3 (𝜏𝜂)
653ad2ant3 1022 . 2 ((𝜑𝜒𝜏) → 𝜂)
72, 4, 63jca 1179 1 ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 982
This theorem is referenced by:  3anim1i  1187  3anim2i  1188  3anim3i  1189  syl3an  1291  syl3anl  1300  spc3egv  2844  spc3gv  2845  eloprabga  5979  le2tri3i  8091  fzmmmeqm  10083  elfz1b  10115  elfz0fzfz0  10151  elfzmlbp  10157  elfzo1  10215  flltdivnn0lt  10330  modmulconst  11857  nndvdslegcd  11993  lgsmulsqcoprm  14884
  Copyright terms: Public domain W3C validator