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

Theorem ad2antrr 472
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)
Hypothesis
Ref Expression
ad2ant.1 (𝜑𝜓)
Assertion
Ref Expression
ad2antrr (((𝜑𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem ad2antrr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantr 270 . 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:  ad3antrrr  476  simpll  496  simplll  500  simpllr  501  vtoclgft  2650  reupick  3255  euotd  4017  frirrg  4113  ralxfrd  4220  foun  5176  f1oprg  5199  dffo4  5347  foeqcnvco  5461  fliftfun  5467  isotr  5487  riotass2  5525  ovmpt2dxf  5657  mpt2xopoveq  5889  tfrlem1  5957  tfrlemibacc  5975  tfrlemibfn  5977  tfrlemi14d  5982  tfrexlem  5983  tfr1onlembacc  5991  tfr1onlembfn  5993  tfr1onlemres  5998  tfrcllembacc  6004  tfrcllembfn  6006  tfrcllemres  6011  frecabcl  6048  nnmordi  6155  eroprf  6265  f1imaen2g  6340  xpen  6386  phplem4dom  6397  nndomo  6399  phpm  6400  fidifsnen  6405  fisbth  6417  en2eqpr  6434  unsnfidcex  6440  unsnfidcel  6441  ordiso2  6505  dfplpq2  6606  nqpi  6630  nqnq0pi  6690  nq0nn  6694  elinp  6726  elnp1st2nd  6728  genprndl  6773  genprndu  6774  addnqprllem  6779  addnqprulem  6780  addnqprl  6781  addnqpru  6782  addlocpr  6788  nqprloc  6797  prmuloc  6818  mulnqprl  6820  mulnqpru  6821  mullocpr  6823  distrlem1prl  6834  distrlem1pru  6835  ltsopr  6848  ltexprlemopl  6853  ltexprlemopu  6855  ltexprlemloc  6859  ltexprlemrl  6862  ltexprlemru  6864  addcanprleml  6866  addcanprlemu  6867  recexprlemloc  6883  recexprlem1ssl  6885  recexprlem1ssu  6886  aptiprleml  6891  aptiprlemu  6892  archpr  6895  cauappcvgprlemm  6897  cauappcvgprlemopl  6898  cauappcvgprlemlol  6899  cauappcvgprlemladdfu  6906  cauappcvgprlemladdfl  6907  cauappcvgprlemladdru  6908  archrecpr  6916  caucvgprlemnkj  6918  caucvgprlemm  6920  caucvgprlemopl  6921  caucvgprlemlol  6922  caucvgprlemdisj  6926  caucvgprlemloc  6927  caucvgprlemladdfu  6929  caucvgprprlemnkltj  6941  caucvgprprlemnkeqj  6942  caucvgprprlemnjltk  6943  caucvgprprlemml  6946  caucvgprprlemopl  6949  caucvgprprlemlol  6950  caucvgprprlemdisj  6954  caucvgprprlemexbt  6958  caucvgprprlemexb  6959  caucvgprprlemaddq  6960  mulgt0sr  7016  caucvgsrlemcau  7031  caucvgsrlemoffcau  7036  caucvgsrlemoffres  7038  axcaucvglemcau  7126  axcaucvglemres  7127  cnegexlem1  7350  cnegex  7353  apsym  7773  apcotr  7774  apadd1  7775  mulext1  7779  mulge0  7786  apti  7789  conjmulap  7884  lemulge11  8011  creui  8104  nndiv  8146  zaddcllemneg  8471  suprzclex  8526  eluzuzle  8708  divfnzn  8787  qapne  8805  xrltso  8947  xrre  8963  xrre3  8965  ixxss12  9005  elioc2  9035  elico2  9036  elicc2  9037  fzm1  9193  fzneuz  9194  eluzgtdifelfzo  9283  elfzonelfzo  9316  exfzdc  9326  qtri3or  9329  exbtwnzlemstep  9334  exbtwnzlemex  9336  exbtwnz  9337  modqid  9431  modqcyc2  9442  modqmuladd  9448  modqmuladdnn0  9450  modaddmodlo  9470  addmodlteq  9480  frecuzrdgrrn  9490  frec2uzrdg  9491  frecuzrdgsuc  9496  frecuzrdgsuctlem  9505  iseqoveq  9540  iseqid3s  9562  expival  9575  expap0  9603  facndiv  9763  faclbnd  9765  ibcval5  9787  sizeunlem  9828  sizeun  9829  sizeprg  9832  ovshftex  9845  2shfti  9857  cjap  9931  caucvgrelemcau  10004  cvg1nlemcau  10008  cvg1nlemres  10009  recvguniq  10019  resqrexlemdecn  10036  resqrexlemcalc3  10040  resqrexlemcvg  10043  resqrexlemoverl  10045  leabs  10098  absexpzap  10104  ltabs  10111  abslt  10112  absle  10113  maxleim  10229  maxabslemval  10232  fimaxre2  10247  minmax  10250  2clim  10278  climshftlemg  10279  climsqz  10311  climsqz2  10312  climrecvg1n  10323  climcvg1nlem  10324  serif0  10327  isumrblem  10337  fisumcvg  10338  nndivides  10347  dvdsext  10400  divalglemeunn  10465  divalglemex  10466  divalglemeuneg  10467  zsupcllemstep  10485  infssuzex  10489  dvdsbnd  10492  bezoutlemnewy  10529  bezoutlemstep  10530  bezoutlemmain  10531  bezoutlemzz  10535  bezoutlemaz  10536  bezoutlembz  10537  bezoutlemeu  10540  bezoutlemle  10541  bezoutlemsup  10542  dfgcd3  10543  dfgcd2  10547  bezoutr1  10566  dvdslcm  10595  lcmgcdlem  10603  qredeq  10622  qredeu  10623  divgcdcoprm0  10627  divgcdcoprmex  10628  cncongr1  10629  isprm2lem  10642  prmind2  10646  exprmfct  10663  prmdvdsfz  10664  prmexpb  10674  rpexp1i  10677  sqrt2irr  10685  sqne2sq  10699  bj-findis  10932  qdencn  10943
  Copyright terms: Public domain W3C validator