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

Theorem 3anim123i 1131
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 967 . 2 ((𝜑𝜒𝜏) → 𝜓)
3 3anim123i.2 . . 3 (𝜒𝜃)
433ad2ant2 968 . 2 ((𝜑𝜒𝜏) → 𝜃)
5 3anim123i.3 . . 3 (𝜏𝜂)
653ad2ant3 969 . 2 ((𝜑𝜒𝜏) → 𝜂)
72, 4, 63jca 1126 1 ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 927
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 929
This theorem is referenced by:  3anim1i  1132  3anim2i  1133  3anim3i  1134  syl3an  1223  syl3anl  1232  spc3egv  2724  spc3gv  2725  eloprabga  5773  le2tri3i  7690  fzmmmeqm  9621  elfz1b  9653  elfz0fzfz0  9686  elfzmlbp  9692  elfzo1  9750  flltdivnn0lt  9860  modmulconst  11270  nndvdslegcd  11399
  Copyright terms: Public domain W3C validator