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

Theorem anim12d 318
Description: Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.)
Hypotheses
Ref Expression
anim12d.1 (φ → (ψχ))
anim12d.2 (φ → (θτ))
Assertion
Ref Expression
anim12d (φ → ((ψ θ) → (χ τ)))

Proof of Theorem anim12d
StepHypRef Expression
1 anim12d.1 . 2 (φ → (ψχ))
2 anim12d.2 . 2 (φ → (θτ))
3 idd 21 . 2 (φ → ((χ τ) → (χ τ)))
41, 2, 3syl2and 279 1 (φ → ((ψ θ) → (χ τ)))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  anim1d  319  anim2d  320  prth  326  im2anan9  517  anim12dan  519  3anim123d  1199  hband  1359  hbbid  1449  spsbim  1706  moim  1946  moimv  1948  2euswapdc  1973  rspcimedv  2635  soss  4025  trin2  4643  xp11m  4686  funss  4846  fun  4988  dff13  5332  f1eqcocnv  5356  isores3  5380  isosolem  5388  f1o2ndf1  5772  tposfn2  5803  tposf1o2  5807  nnaordex  6011  recexprlemss1l  6469  recexprlemss1u  6470
  Copyright terms: Public domain W3C validator