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

Theorem anim12d 331
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 291 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
ta ) ) )
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  332  anim2d  333  anim12  339  im2anan9  570  anim12dan  572  3anim123d  1280  hband  1448  hbbid  1537  spsbim  1797  moim  2039  moimv  2041  2euswapdc  2066  rspcimedv  2763  soss  4204  trin2  4898  xp11m  4945  funss  5110  fun  5263  dff13  5635  f1eqcocnv  5658  isores3  5682  isosolem  5691  f1o2ndf1  6091  tposfn2  6129  tposf1o2  6133  nndifsnid  6369  nnaordex  6389  supmoti  6846  isotilem  6859  recexprlemss1l  7407  recexprlemss1u  7408  caucvgsrlemoffres  7572  suplocsrlem  7580  nnindnn  7665  eqord1  8209  lemul12b  8576  lt2msq  8601  lbreu  8660  cju  8676  nnind  8693  uz11  9297  xrre2  9544  ico0  9979  ioc0  9980  expcan  10403  gcdaddm  11568  bezoutlemaz  11587  bezoutlembz  11588  isprm3  11695  epttop  12154  cnptopresti  12302  cnptoprest  12303  txcnp  12335  addcncntoplem  12615  mulcncflem  12654  bj-stand  12767  exmidsbthrlem  13028
  Copyright terms: Public domain W3C validator