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  530  anim12dan  532  3anim123d  1213  hband  1375  hbbid  1464  spsbim  1721  moim  1961  moimv  1963  2euswapdc  1988  rspcimedv  2652  soss  4042  trin2  4659  xp11m  4702  funss  4863  fun  5006  dff13  5350  f1eqcocnv  5374  isores3  5398  isosolem  5406  f1o2ndf1  5791  tposfn2  5822  tposf1o2  5826  nnaordex  6036  recexprlemss1l  6605  recexprlemss1u  6606  lemul12b  7568  lt2msq  7593  cju  7654  nnind  7671  uz11  8231  xrre2  8464
  Copyright terms: Public domain W3C validator