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

Theorem ad2ant2r 493
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 463 . 2 ((𝜑 ∧ (𝜓𝜏)) → 𝜒)
32adantlr 461 1 (((𝜑𝜃) ∧ (𝜓𝜏)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  foco  5191  fvco4  5321  fliftfun  5515  f1imaen2g  6440  fodjuomnilem0  6707  mulcomnqg  6845  mulassnqg  6846  ltdcnq  6859  lt2addnq  6866  lt2mulnq  6867  enq0ref  6895  enq0tr  6896  addcmpblnq0  6905  nqpnq0nq  6915  nqnq0m  6917  mulcomnq0  6922  addlocpr  6998  nqprl  7013  nqpru  7014  prmuloc  7028  distrlem1prl  7044  distrlem1pru  7045  ltaddpr  7059  ltexprlemopu  7065  ltexprlemdisj  7068  ltexprlemloc  7069  ltexprlemrl  7072  ltexprlemru  7074  recexprlemloc  7093  recexprlem1ssl  7095  recexprlem1ssu  7096  caucvgprprlemopu  7161  addcomsrg  7204  mulcomsrg  7206  mulasssrg  7207  distrsrg  7208  addcnsr  7274  mulcnsr  7275  addcnsrec  7282  axaddcl  7304  axaddcom  7308  addsub4  7628  muladd  7765  mullt0  7861  apreim  7980  mulge0  7996  divmuldivap  8077  divmul24ap  8081  divmuleqap  8082  recdivap  8083  divadddivap  8092  conjmulap  8094  prodgt0gt0  8206  ltmul12a  8215  lemul12b  8216  lediv2a  8250  qmulcl  9017  irrmul  9027  xrrege0  9182  ge0addcl  9294  ge0mulcl  9295  fzass4  9370  fzrev  9391  fzocatel  9499  serige0  9789  expclzaplem  9816  expge0  9828  expge1  9829  lt2sq  9865  le2sq  9866  bernneq  9909  sq11ap  9955  sqrt11ap  10298  2clim  10514  climge0  10537  opeo  10677  omeo  10678  cncongr1  10865
  Copyright terms: Public domain W3C validator