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

Theorem anim12d 333
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 293 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  anim1d  334  anim2d  335  anim12  341  im2anan9  587  anim12dan  589  3anim123d  1297  hband  1465  hbbid  1554  spsbim  1815  moim  2063  moimv  2065  2euswapdc  2090  rspcimedv  2791  soss  4236  trin2  4930  xp11m  4977  funss  5142  fun  5295  dff13  5669  f1eqcocnv  5692  isores3  5716  isosolem  5725  f1o2ndf1  6125  tposfn2  6163  tposf1o2  6167  nndifsnid  6403  nnaordex  6423  supmoti  6880  isotilem  6893  recexprlemss1l  7450  recexprlemss1u  7451  caucvgsrlemoffres  7615  suplocsrlem  7623  nnindnn  7708  eqord1  8252  lemul12b  8626  lt2msq  8651  lbreu  8710  cju  8726  nnind  8743  uz11  9355  xrre2  9611  ico0  10046  ioc0  10047  expcan  10470  gcdaddm  11678  bezoutlemaz  11697  bezoutlembz  11698  isprm3  11805  epttop  12268  cnptopresti  12416  cnptoprest  12417  txcnp  12449  addcncntoplem  12729  mulcncflem  12768  bj-stand  13009  exmidsbthrlem  13270
  Copyright terms: Public domain W3C validator