ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anim12d Unicode 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  |-  ( ph  ->  ( ps  ->  ch ) )
anim12d.2  |-  ( ph  ->  ( th  ->  ta ) )
Assertion
Ref Expression
anim12d  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
ta ) ) )

Proof of Theorem anim12d
StepHypRef Expression
1 anim12d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 anim12d.2 . 2  |-  ( ph  ->  ( th  ->  ta ) )
3 idd 21 . 2  |-  ( ph  ->  ( ( ch  /\  ta )  ->  ( ch 
/\  ta ) ) )
41, 2, 3syl2and 289 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
ta ) ) )
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  565  anim12dan  567  3anim123d  1255  hband  1423  hbbid  1512  spsbim  1771  moim  2012  moimv  2014  2euswapdc  2039  rspcimedv  2724  soss  4132  trin2  4810  xp11m  4856  funss  5020  fun  5168  dff13  5529  f1eqcocnv  5552  isores3  5576  isosolem  5585  f1o2ndf1  5975  tposfn2  6013  tposf1o2  6017  nndifsnid  6246  nnaordex  6266  supmoti  6667  isotilem  6680  recexprlemss1l  7173  recexprlemss1u  7174  caucvgsrlemoffres  7324  nnindnn  7407  lemul12b  8294  lt2msq  8319  lbreu  8378  cju  8393  nnind  8410  uz11  9010  xrre2  9252  ico0  9638  ioc0  9639  expcan  10090  gcdaddm  11068  bezoutlemaz  11085  bezoutlembz  11086  isprm3  11193  exmidsbthrlem  11569
  Copyright terms: Public domain W3C validator