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

Theorem ad2antrl 481
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 274 . 2 ((𝜑𝜃) → 𝜓)
32adantl 275 1 ((𝜒 ∧ (𝜑𝜃)) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  simprl  505  simprll  511  simprlr  512  elxp5  4997  f1oprg  5379  cnvf1olem  6089  tfrcl  6229  nnaordi  6372  swoer  6425  0er  6431  mapxpen  6710  fict  6730  dif1enen  6742  php5fin  6744  fin0  6747  fin0or  6748  diffisn  6755  infnfi  6757  unsnfi  6775  fidcenumlemrk  6810  sbthlemi8  6820  fiuni  6834  supmoti  6848  eldju2ndl  6925  eldju2ndr  6926  omp1eomlem  6947  difinfsnlem  6952  ctmlemr  6961  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  enq0sym  7208  nqnq0pi  7214  addlocpr  7312  nqprl  7327  addnqprlemrl  7333  addnqprlemru  7334  mulnqprlemrl  7349  mulnqprlemru  7350  archpr  7419  cauappcvgprlemloc  7428  cauappcvgprlemladdfl  7431  archrecpr  7440  caucvgprlemdisj  7450  caucvgprlemloc  7451  caucvgprprlemml  7470  caucvgprprlemopl  7473  caucvgprprlemdisj  7478  caucvgprprlemloc  7479  suplocexprlemmu  7494  suplocexprlemdisj  7496  mulcmpblnrlemg  7516  caucvgsrlemgt1  7571  axarch  7667  axcaucvglemres  7675  cnegexlem2  7906  mulge0  8349  divdivap1  8451  divdivap2  8452  conjmulap  8457  ltdivmul  8602  nn0ge0div  9106  peano2uz2  9126  peano5uzti  9127  eluzp1m1  9317  xleadd1a  9624  iooshf  9703  divelunit  9753  eluzgtdifelfzo  9942  ioom  10006  modqcyc2  10101  modaddmodup  10128  uzennn  10177  seq3fveq2  10210  seq3id2  10250  seqfeq3  10253  expineg2  10270  mulexpzap  10301  leexp2r  10315  expnlbnd2  10385  hashfacen  10547  resqrexlemp1rp  10746  resqrexlemfp1  10749  negfi  10967  climcaucn  11088  fsum3cvg3  11133  fsum2dlemstep  11171  mptfzshft  11179  expcnvre  11240  moddvds  11429  dvdsflip  11476  addmodlteqALT  11484  nn0o  11531  zsupcllemex  11566  dfgcd2  11629  lcmgcdlem  11685  cncongr1  11711  prmind2  11728  isprm6  11752  cncongrprm  11762  oddpwdclemdc  11778  sqrt2irrap  11785  hashdvds  11824  crth  11827  hashgcdlem  11830  hashgcdeq  11831  ennnfonelemex  11854  setscom  11926  tgcl  12160  lmbr2  12310  txcn  12371  txdis1cn  12374  txlm  12375  hmeoimaf1o  12410  txhmeo  12415  bl2in  12499  blssps  12523  blss  12524  blssexps  12525  blssex  12526  bdxmet  12597  xmetxp  12603  xmetxpbl  12604  xmettx  12606  metcnp3  12607  metcnpi3  12613  dedekindicc  12707  limcimolemlt  12729  qdencn  13149  trilpolemlt1  13161
  Copyright terms: Public domain W3C validator