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

Theorem ad2ant2r 500
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
ad2ant2.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
ad2ant2r  |-  ( ( ( ph  /\  th )  /\  ( ps  /\  ta ) )  ->  ch )

Proof of Theorem ad2ant2r
StepHypRef Expression
1 ad2ant2.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21adantrr 470 . 2  |-  ( (
ph  /\  ( ps  /\ 
ta ) )  ->  ch )
32adantlr 468 1  |-  ( ( ( ph  /\  th )  /\  ( ps  /\  ta ) )  ->  ch )
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 is referenced by:  foco  5325  fvco4  5461  fliftfun  5665  f1imaen2g  6655  fodju0  6987  mulcomnqg  7159  mulassnqg  7160  ltdcnq  7173  lt2addnq  7180  lt2mulnq  7181  enq0ref  7209  enq0tr  7210  addcmpblnq0  7219  nqpnq0nq  7229  nqnq0m  7231  mulcomnq0  7236  addlocpr  7312  nqprl  7327  nqpru  7328  prmuloc  7342  distrlem1prl  7358  distrlem1pru  7359  ltaddpr  7373  ltexprlemopu  7379  ltexprlemdisj  7382  ltexprlemloc  7383  ltexprlemrl  7386  ltexprlemru  7388  recexprlemloc  7407  recexprlem1ssl  7409  recexprlem1ssu  7410  caucvgprprlemopu  7475  addcomsrg  7531  mulcomsrg  7533  mulasssrg  7534  distrsrg  7535  addcnsr  7610  mulcnsr  7611  addcnsrec  7618  axaddcl  7640  axaddcom  7646  addsub4  7973  muladd  8114  mullt0  8210  apreim  8333  mulge0  8349  divmuldivap  8440  divmul24ap  8444  divmuleqap  8445  recdivap  8446  divadddivap  8455  conjmulap  8457  prodgt0gt0  8577  ltmul12a  8586  lemul12b  8587  lediv2a  8621  qmulcl  9397  irrmul  9407  xrrege0  9576  ge0addcl  9732  ge0mulcl  9733  ge0xaddcl  9734  fzass4  9810  fzrev  9832  fzocatel  9944  expclzaplem  10285  expge0  10297  expge1  10298  lt2sq  10334  le2sq  10335  bernneq  10380  sq11ap  10426  sqrt11ap  10778  2clim  11038  climge0  11062  tanaddaplem  11372  opeo  11521  omeo  11522  cncongr1  11711  ennnfonelemf1  11858  setscom  11926  opnneissb  12251  cncnpi  12324  neitx  12364  txcnmpt  12369  txrest  12372  txdis1cn  12374  ptolemy  12832
  Copyright terms: Public domain W3C validator