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  8332  mulge0  8348  divmuldivap  8439  divmul24ap  8443  divmuleqap  8444  recdivap  8445  divadddivap  8454  conjmulap  8456  prodgt0gt0  8573  ltmul12a  8582  lemul12b  8583  lediv2a  8617  qmulcl  9385  irrmul  9395  xrrege0  9563  ge0addcl  9719  ge0mulcl  9720  ge0xaddcl  9721  fzass4  9797  fzrev  9819  fzocatel  9931  expclzaplem  10272  expge0  10284  expge1  10285  lt2sq  10321  le2sq  10322  bernneq  10367  sq11ap  10413  sqrt11ap  10765  2clim  11025  climge0  11049  tanaddaplem  11359  opeo  11506  omeo  11507  cncongr1  11696  ennnfonelemf1  11842  setscom  11910  opnneissb  12235  cncnpi  12308  neitx  12348  txcnmpt  12353  txrest  12356  txdis1cn  12358  ptolemy  12816
  Copyright terms: Public domain W3C validator