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

Theorem 3anim123i 1184
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 1018 . 2 ((𝜑𝜒𝜏) → 𝜓)
3 3anim123i.2 . . 3 (𝜒𝜃)
433ad2ant2 1019 . 2 ((𝜑𝜒𝜏) → 𝜃)
5 3anim123i.3 . . 3 (𝜏𝜂)
653ad2ant3 1020 . 2 ((𝜑𝜒𝜏) → 𝜂)
72, 4, 63jca 1177 1 ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 978
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 980
This theorem is referenced by:  3anim1i  1185  3anim2i  1186  3anim3i  1187  syl3an  1280  syl3anl  1289  spc3egv  2830  spc3gv  2831  eloprabga  5962  le2tri3i  8066  fzmmmeqm  10058  elfz1b  10090  elfz0fzfz0  10126  elfzmlbp  10132  elfzo1  10190  flltdivnn0lt  10304  modmulconst  11830  nndvdslegcd  11966  lgsmulsqcoprm  14450
  Copyright terms: Public domain W3C validator