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

Theorem ad2ant2r 486
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 456 . 2  |-  ( (
ph  /\  ( ps  /\ 
ta ) )  ->  ch )
32adantlr 454 1  |-  ( ( ( ph  /\  th )  /\  ( ps  /\  ta ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  foco  5144  fliftfun  5464  f1imaen2g  6304  mulcomnqg  6539  mulassnqg  6540  ltdcnq  6553  lt2addnq  6560  lt2mulnq  6561  enq0ref  6589  enq0tr  6590  addcmpblnq0  6599  nqpnq0nq  6609  nqnq0m  6611  mulcomnq0  6616  addlocpr  6692  nqprl  6707  nqpru  6708  prmuloc  6722  distrlem1prl  6738  distrlem1pru  6739  ltaddpr  6753  ltexprlemopu  6759  ltexprlemdisj  6762  ltexprlemloc  6763  ltexprlemrl  6766  ltexprlemru  6768  recexprlemloc  6787  recexprlem1ssl  6789  recexprlem1ssu  6790  caucvgprprlemopu  6855  addcomsrg  6898  mulcomsrg  6900  mulasssrg  6901  distrsrg  6902  addcnsr  6968  mulcnsr  6969  addcnsrec  6976  axaddcl  6998  axaddcom  7002  addsub4  7317  muladd  7453  mullt0  7549  apreim  7668  mulge0  7684  divmuldivap  7763  divmul24ap  7767  divmuleqap  7768  recdivap  7769  divadddivap  7778  conjmulap  7780  prodgt0gt0  7892  ltmul12a  7901  lemul12b  7902  lediv2a  7936  qmulcl  8669  irrmul  8679  xrrege0  8839  ge0addcl  8951  ge0mulcl  8952  fzass4  9027  fzrev  9048  fzocatel  9157  serige0  9417  expclzaplem  9444  expge0  9456  expge1  9457  lt2sq  9493  le2sq  9494  bernneq  9537  sq11ap  9583  sqrt11ap  9865  2clim  10053  climge0  10076  opeo  10209  omeo  10210
  Copyright terms: Public domain W3C validator