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

Theorem anim12d 329
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 290 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  anim1d  330  anim2d  331  prth  337  im2anan9  566  anim12dan  568  3anim123d  1256  hband  1424  hbbid  1513  spsbim  1772  moim  2013  moimv  2015  2euswapdc  2040  rspcimedv  2725  soss  4150  trin2  4836  xp11m  4882  funss  5047  fun  5196  dff13  5561  f1eqcocnv  5584  isores3  5608  isosolem  5617  f1o2ndf1  6007  tposfn2  6045  tposf1o2  6049  nndifsnid  6280  nnaordex  6300  supmoti  6742  isotilem  6755  recexprlemss1l  7255  recexprlemss1u  7256  caucvgsrlemoffres  7406  nnindnn  7489  eqord1  8022  lemul12b  8383  lt2msq  8408  lbreu  8467  cju  8482  nnind  8499  uz11  9102  xrre2  9344  ico0  9734  ioc0  9735  expcan  10186  gcdaddm  11314  bezoutlemaz  11331  bezoutlembz  11332  isprm3  11439  epttop  11851  exmidsbthrlem  12184
  Copyright terms: Public domain W3C validator