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

Theorem anim12d 328
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 289 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  anim1d  329  anim2d  330  prth  336  im2anan9  563  anim12dan  565  3anim123d  1253  hband  1421  hbbid  1510  spsbim  1768  moim  2009  moimv  2011  2euswapdc  2036  rspcimedv  2717  soss  4114  trin2  4787  xp11m  4832  funss  4996  fun  5141  dff13  5502  f1eqcocnv  5525  isores3  5549  isosolem  5558  f1o2ndf1  5944  tposfn2  5979  tposf1o2  5983  nndifsnid  6212  nnaordex  6232  supmoti  6625  isotilem  6638  recexprlemss1l  7131  recexprlemss1u  7132  caucvgsrlemoffres  7282  nnindnn  7365  lemul12b  8250  lt2msq  8275  lbreu  8334  cju  8349  nnind  8366  uz11  8966  xrre2  9208  ico0  9594  ioc0  9595  expcan  10014  gcdaddm  10842  bezoutlemaz  10859  bezoutlembz  10860  isprm3  10967  exmidsbthrlem  11342
  Copyright terms: Public domain W3C validator