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

Theorem ad2ant2r 498
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 468 . 2  |-  ( (
ph  /\  ( ps  /\ 
ta ) )  ->  ch )
32adantlr 466 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  5323  fvco4  5459  fliftfun  5663  f1imaen2g  6653  fodju0  6985  mulcomnqg  7155  mulassnqg  7156  ltdcnq  7169  lt2addnq  7176  lt2mulnq  7177  enq0ref  7205  enq0tr  7206  addcmpblnq0  7215  nqpnq0nq  7225  nqnq0m  7227  mulcomnq0  7232  addlocpr  7308  nqprl  7323  nqpru  7324  prmuloc  7338  distrlem1prl  7354  distrlem1pru  7355  ltaddpr  7369  ltexprlemopu  7375  ltexprlemdisj  7378  ltexprlemloc  7379  ltexprlemrl  7382  ltexprlemru  7384  recexprlemloc  7403  recexprlem1ssl  7405  recexprlem1ssu  7406  caucvgprprlemopu  7471  addcomsrg  7527  mulcomsrg  7529  mulasssrg  7530  distrsrg  7531  addcnsr  7606  mulcnsr  7607  addcnsrec  7614  axaddcl  7636  axaddcom  7642  addsub4  7969  muladd  8110  mullt0  8206  apreim  8328  mulge0  8344  divmuldivap  8435  divmul24ap  8439  divmuleqap  8440  recdivap  8441  divadddivap  8450  conjmulap  8452  prodgt0gt0  8569  ltmul12a  8578  lemul12b  8579  lediv2a  8613  qmulcl  9381  irrmul  9391  xrrege0  9559  ge0addcl  9715  ge0mulcl  9716  ge0xaddcl  9717  fzass4  9793  fzrev  9815  fzocatel  9927  expclzaplem  10268  expge0  10280  expge1  10281  lt2sq  10317  le2sq  10318  bernneq  10363  sq11ap  10409  sqrt11ap  10761  2clim  11021  climge0  11045  tanaddaplem  11355  opeo  11501  omeo  11502  cncongr1  11691  ennnfonelemf1  11837  setscom  11905  opnneissb  12230  cncnpi  12303  neitx  12343  txcnmpt  12348  txrest  12351  txdis1cn  12353
  Copyright terms: Public domain W3C validator