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

Theorem ad2ant2rl 511
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007.)
Hypothesis
Ref Expression
ad2ant2.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
ad2ant2rl (((𝜑𝜃) ∧ (𝜏𝜓)) → 𝜒)

Proof of Theorem ad2ant2rl
StepHypRef Expression
1 ad2ant2.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantrl 478 . 2 ((𝜑 ∧ (𝜏𝜓)) → 𝜒)
32adantlr 477 1 (((𝜑𝜃) ∧ (𝜏𝜓)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem is referenced by:  fvtp1g  5745  fcof1o  5811  infnfi  6924  addcomnqg  7411  addassnqg  7412  nqtri3or  7426  ltexnqq  7438  nqnq0pi  7468  nqpnq0nq  7483  nqnq0a  7484  addassnq0lemcl  7491  ltaddpr  7627  ltexprlemloc  7637  addcanprlemu  7645  recexprlem1ssu  7664  aptiprleml  7669  mulcomsrg  7787  mulasssrg  7788  distrsrg  7789  aptisr  7809  mulcnsr  7865  cnegex  8166  muladd  8372  lemul12b  8849  qaddcl  9667  iooshf  9984  elfzomelpfzo  10263  expnegzap  10588  setscom  12555  grplmulf1o  13033  lmodfopne  13659  cnpnei  14196  cxplt3  14817  cxple3  14818
  Copyright terms: Public domain W3C validator