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  520  simprll  526  simprlr  527  elxp5  5027  f1oprg  5411  cnvf1olem  6121  tfrcl  6261  nnaordi  6404  swoer  6457  0er  6463  mapxpen  6742  fict  6762  dif1enen  6774  php5fin  6776  fin0  6779  fin0or  6780  diffisn  6787  infnfi  6789  unsnfi  6807  fidcenumlemrk  6842  sbthlemi8  6852  fiuni  6866  supmoti  6880  eldju2ndl  6957  eldju2ndr  6958  omp1eomlem  6979  difinfsnlem  6984  ctmlemr  6993  exmidfodomrlemr  7063  exmidfodomrlemrALT  7064  enq0sym  7252  nqnq0pi  7258  addlocpr  7356  nqprl  7371  addnqprlemrl  7377  addnqprlemru  7378  mulnqprlemrl  7393  mulnqprlemru  7394  archpr  7463  cauappcvgprlemloc  7472  cauappcvgprlemladdfl  7475  archrecpr  7484  caucvgprlemdisj  7494  caucvgprlemloc  7495  caucvgprprlemml  7514  caucvgprprlemopl  7517  caucvgprprlemdisj  7522  caucvgprprlemloc  7523  suplocexprlemmu  7538  suplocexprlemdisj  7540  mulcmpblnrlemg  7560  caucvgsrlemgt1  7615  axarch  7711  axcaucvglemres  7719  cnegexlem2  7950  mulge0  8393  divdivap1  8495  divdivap2  8496  conjmulap  8501  ltdivmul  8646  nn0ge0div  9150  peano2uz2  9170  peano5uzti  9171  eluzp1m1  9361  xleadd1a  9668  iooshf  9747  divelunit  9797  eluzgtdifelfzo  9986  ioom  10050  modqcyc2  10145  modaddmodup  10172  uzennn  10221  seq3fveq2  10254  seq3id2  10294  seqfeq3  10297  expineg2  10314  mulexpzap  10345  leexp2r  10359  expnlbnd2  10429  hashfacen  10591  resqrexlemp1rp  10790  resqrexlemfp1  10793  negfi  11011  climcaucn  11132  fsum3cvg3  11177  fsum2dlemstep  11215  mptfzshft  11223  expcnvre  11284  moddvds  11513  dvdsflip  11560  addmodlteqALT  11568  nn0o  11615  zsupcllemex  11650  dfgcd2  11713  lcmgcdlem  11769  cncongr1  11795  prmind2  11812  isprm6  11836  cncongrprm  11846  oddpwdclemdc  11862  sqrt2irrap  11869  hashdvds  11908  crth  11911  hashgcdlem  11914  hashgcdeq  11915  ennnfonelemex  11938  setscom  12013  tgcl  12247  lmbr2  12397  txcn  12458  txdis1cn  12461  txlm  12462  hmeoimaf1o  12497  txhmeo  12502  bl2in  12586  blssps  12610  blss  12611  blssexps  12612  blssex  12613  bdxmet  12684  xmetxp  12690  xmetxpbl  12691  xmettx  12693  metcnp3  12694  metcnpi3  12700  dedekindicc  12794  limcimolemlt  12816  qdencn  13329  trilpolemlt1  13341
  Copyright terms: Public domain W3C validator