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

Theorem ad2ant2r 478
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
ad2ant2.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
ad2ant2r (((𝜑𝜃) ∧ (𝜓𝜏)) → 𝜒)

Proof of Theorem ad2ant2r
StepHypRef Expression
1 ad2ant2.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantrr 448 . 2 ((𝜑 ∧ (𝜓𝜏)) → 𝜒)
32adantlr 446 1 (((𝜑𝜃) ∧ (𝜓𝜏)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  foco  5116  fliftfun  5436  f1imaen2g  6273  mulcomnqg  6481  mulassnqg  6482  ltdcnq  6495  lt2addnq  6502  lt2mulnq  6503  enq0ref  6531  enq0tr  6532  addcmpblnq0  6541  nqpnq0nq  6551  nqnq0m  6553  mulcomnq0  6558  addlocpr  6634  nqprl  6649  nqpru  6650  prmuloc  6664  distrlem1prl  6680  distrlem1pru  6681  ltaddpr  6695  ltexprlemopu  6701  ltexprlemdisj  6704  ltexprlemloc  6705  ltexprlemrl  6708  ltexprlemru  6710  recexprlemloc  6729  recexprlem1ssl  6731  recexprlem1ssu  6732  caucvgprprlemopu  6797  addcomsrg  6840  mulcomsrg  6842  mulasssrg  6843  distrsrg  6844  addcnsr  6910  mulcnsr  6911  addcnsrec  6918  axaddcl  6940  axaddcom  6944  addsub4  7254  muladd  7381  mullt0  7475  apreim  7594  mulge0  7610  divmuldivap  7688  divmul24ap  7692  divmuleqap  7693  recdivap  7694  divadddivap  7703  conjmulap  7705  prodgt0gt0  7817  ltmul12a  7826  lemul12b  7827  lediv2a  7861  qmulcl  8572  irrmul  8581  xrrege0  8738  ge0addcl  8850  ge0mulcl  8851  fzass4  8925  fzrev  8946  fzocatel  9055  serige0  9252  expclzaplem  9279  expge0  9291  expge1  9292  lt2sq  9327  le2sq  9328  bernneq  9369  sq11ap  9414  sqrt11ap  9636  2clim  9822  climge0  9845
  Copyright terms: Public domain W3C validator