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

Theorem anim12d 322
 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 283 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101 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 This theorem is referenced by:  anim1d  323  anim2d  324  prth  330  im2anan9  540  anim12dan  542  3anim123d  1225  hband  1394  hbbid  1483  spsbim  1740  moim  1980  moimv  1982  2euswapdc  2007  rspcimedv  2675  soss  4079  trin2  4744  xp11m  4787  funss  4948  fun  5091  dff13  5435  f1eqcocnv  5459  isores3  5483  isosolem  5491  f1o2ndf1  5877  tposfn2  5912  tposf1o2  5916  nnaordex  6131  supmoti  6399  isotilem  6410  recexprlemss1l  6791  recexprlemss1u  6792  caucvgsrlemoffres  6942  nnindnn  7025  lemul12b  7902  lt2msq  7927  cju  7989  nnind  8006  uz11  8591  xrre2  8835  ico0  9218  ioc0  9219
 Copyright terms: Public domain W3C validator