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

Theorem ad2ant2lr 507
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.)
Hypothesis
Ref Expression
ad2ant2.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
ad2ant2lr  |-  ( ( ( th  /\  ph )  /\  ( ps  /\  ta ) )  ->  ch )

Proof of Theorem ad2ant2lr
StepHypRef Expression
1 ad2ant2.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21adantrr 476 . 2  |-  ( (
ph  /\  ( ps  /\ 
ta ) )  ->  ch )
32adantll 473 1  |-  ( ( ( th  /\  ph )  /\  ( 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:  mpteqb  5584  fiunsnnn  6855  addcomnqg  7330  addassnqg  7331  nqtri3or  7345  lt2addnq  7353  lt2mulnq  7354  enq0ref  7382  enq0tr  7383  nqnq0pi  7387  nqpnq0nq  7402  nqnq0a  7403  distrnq0  7408  addassnq0lemcl  7410  ltsrprg  7696  mulcomsrg  7706  mulasssrg  7707  distrsrg  7708  aptisr  7728  mulcnsr  7784  cnegex  8084  sub4  8151  muladd  8290  ltleadd  8352  divdivdivap  8617  divadddivap  8631  ltmul12a  8763  fzrev  10027  facndiv  10660  cncongr1  12044  blbas  13148  cncfmet  13294  ptolemy  13460
  Copyright terms: Public domain W3C validator