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

Theorem 3anim123i 1100
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 936 . 2 ((𝜑𝜒𝜏) → 𝜓)
3 3anim123i.2 . . 3 (𝜒𝜃)
433ad2ant2 937 . 2 ((𝜑𝜒𝜏) → 𝜃)
5 3anim123i.3 . . 3 (𝜏𝜂)
653ad2ant3 938 . 2 ((𝜑𝜒𝜏) → 𝜂)
72, 4, 63jca 1095 1 ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  3anim1i  1101  3anim2i  1102  3anim3i  1103  syl3an  1188  syl3anl  1197  spc3egv  2661  spc3gv  2662  eloprabga  5619  le2tri3i  7185  fzmmmeqm  9023  elfz1b  9054  elfz0fzfz0  9085  elfzmlbmOLD  9091  elfzmlbp  9092  elfzo1  9148  flltdivnn0lt  9254  modmulconst  10139
  Copyright terms: Public domain W3C validator