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

Theorem ad2antrl 474
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
Hypothesis
Ref Expression
ad2ant.1 (𝜑𝜓)
Assertion
Ref Expression
ad2antrl ((𝜒 ∧ (𝜑𝜃)) → 𝜓)

Proof of Theorem ad2antrl
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantr 270 . 2 ((𝜑𝜃) → 𝜓)
32adantl 271 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:  simprl  498  simprll  504  simprlr  505  elxp5  4839  f1oprg  5199  cnvf1olem  5876  tfrcl  6013  nnaordi  6147  swoer  6200  0er  6206  fict  6403  php5fin  6416  fin0  6419  fin0or  6420  diffisn  6427  infnfi  6429  unsnfi  6439  supmoti  6465  enq0sym  6684  nqnq0pi  6690  addlocpr  6788  nqprl  6803  addnqprlemrl  6809  addnqprlemru  6810  mulnqprlemrl  6825  mulnqprlemru  6826  archpr  6895  cauappcvgprlemloc  6904  cauappcvgprlemladdfl  6907  archrecpr  6916  caucvgprlemdisj  6926  caucvgprlemloc  6927  caucvgprprlemml  6946  caucvgprprlemopl  6949  caucvgprprlemdisj  6954  caucvgprprlemloc  6955  mulcmpblnrlemg  6979  caucvgsrlemgt1  7033  axarch  7119  axcaucvglemres  7127  cnegexlem2  7351  mulge0  7786  divdivap1  7878  divdivap2  7879  conjmulap  7884  ltdivmul  8021  nn0ge0div  8515  peano2uz2  8535  peano5uzti  8536  eluzp1m1  8723  iooshf  9051  divelunit  9100  eluzgtdifelfzo  9283  ioom  9347  modqcyc2  9442  modaddmodup  9469  iseqval  9530  iseqfveq2  9544  iseqid2  9564  expineg2  9582  mulexpzap  9613  leexp2r  9627  expnlbnd2  9695  resqrexlemp1rp  10030  resqrexlemfp1  10033  negfi  10248  climcaucn  10326  moddvds  10349  dvdsflip  10396  addmodlteqALT  10404  nn0o  10451  zsupcllemex  10486  dfgcd2  10547  lcmgcdlem  10603  cncongr1  10629  prmind2  10646  isprm6  10670  cncongrprm  10680  oddpwdclemdc  10695  sqrt2irrap  10702  qdencn  10943
  Copyright terms: Public domain W3C validator