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

Theorem anim12dan 604
Description: Conjoin antecedents and consequents in a deduction. (Contributed by Mario Carneiro, 12-May-2014.)
Hypotheses
Ref Expression
anim12dan.1 ((𝜑𝜓) → 𝜒)
anim12dan.2 ((𝜑𝜃) → 𝜏)
Assertion
Ref Expression
anim12dan ((𝜑 ∧ (𝜓𝜃)) → (𝜒𝜏))

Proof of Theorem anim12dan
StepHypRef Expression
1 anim12dan.1 . . . 4 ((𝜑𝜓) → 𝜒)
21ex 115 . . 3 (𝜑 → (𝜓𝜒))
3 anim12dan.2 . . . 4 ((𝜑𝜃) → 𝜏)
43ex 115 . . 3 (𝜑 → (𝜃𝜏))
52, 4anim12d 335 . 2 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
65imp 124 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-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  xpexr2m  5178  isocnv  5952  f1oiso  5967  f1oiso2  5968  f1o2ndf1  6393  xpf1o  7030  pc11  12906  imasaddfnlemg  13399  imasaddflemg  13401  mhmpropd  13551  ghmsub  13840  invrpropdg  14166  znidom  14674  tgclb  14792  innei  14890  txcn  15002  plymullem1  15475  lgsdir2  15765
  Copyright terms: Public domain W3C validator