ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ad2ant2r Structured version   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  5059  fliftfun  5379  f1imaen2g  6209  mulcomnqg  6367  mulassnqg  6368  ltdcnq  6381  lt2addnq  6388  enq0ref  6416  enq0tr  6417  addcmpblnq0  6426  nqpnq0nq  6436  nqnq0m  6438  mulcomnq0  6443  addlocpr  6519  nqprl  6533  prmuloc  6547  distrlem1prl  6558  distrlem1pru  6559  ltaddpr  6571  ltexprlemopu  6577  ltexprlemdisj  6580  ltexprlemloc  6581  ltexprlemrl  6584  ltexprlemru  6586  recexprlemloc  6603  recexprlem1ssl  6605  recexprlem1ssu  6606  addcomsrg  6683  mulcomsrg  6685  mulasssrg  6686  distrsrg  6687  addcnsr  6731  mulcnsr  6732  addcnsrec  6739  axaddcl  6750  axaddcom  6754  addsub4  7050  muladd  7177  mullt0  7270  apreim  7387  mulge0  7403  divmuldivap  7470  divmul24ap  7474  divmuleqap  7475  recdivap  7476  divadddivap  7485  conjmulap  7487  prodgt0gt0  7598  ltmul12a  7607  lemul12b  7608  lediv2a  7642  qmulcl  8348  irrmul  8356  xrrege0  8508  ge0addcl  8620  ge0mulcl  8621  fzass4  8695  fzrev  8716  fzocatel  8825  expclzaplem  8933  expge0  8945  expge1  8946  lt2sq  8980  le2sq  8981  bernneq  9022
  Copyright terms: Public domain W3C validator