Theorem ad2antrl 490

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

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 276	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜓)
3	2	adantl 277	1 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  simprl  531  simprll  539  simprlr  540  elxp5  5258  f1oprg  5667  elovmporab1w  6265  cnvf1olem  6435  ressuppss  6469  tfrcl  6610  nnaordi  6756  swoer  6810  0er  6816  modom  7076  pw2f1odclem  7102  mapxpen  7116  mapunen  7119  fict  7138  dif1enen  7152  php5fin  7154  fin0  7157  fin0or  7158  diffisn  7165  infnfi  7167  unsnfi  7194  fidcenumlemrk  7239  sbthlemi8  7249  fiuni  7280  2omap  7284  supmoti  7299  eldju2ndl  7378  eldju2ndr  7379  omp1eomlem  7400  difinfsnlem  7405  ctmlemr  7414  nninfninc  7429  nninfwlpor  7480  exmidfodomrlemr  7520  exmidfodomrlemrALT  7521  enq0sym  7765  nqnq0pi  7771  addlocpr  7869  nqprl  7884  addnqprlemrl  7890  addnqprlemru  7891  mulnqprlemrl  7906  mulnqprlemru  7907  archpr  7976  cauappcvgprlemloc  7985  cauappcvgprlemladdfl  7988  archrecpr  7997  caucvgprlemdisj  8007  caucvgprlemloc  8008  caucvgprprlemml  8027  caucvgprprlemopl  8030  caucvgprprlemdisj  8035  caucvgprprlemloc  8036  suplocexprlemmu  8051  suplocexprlemdisj  8053  mulcmpblnrlemg  8073  caucvgsrlemgt1  8128  axarch  8224  axcaucvglemres  8232  cnegexlem2  8468  mulge0  8913  divdivap1  9019  divdivap2  9020  conjmulap  9025  ltdivmul  9172  nn0ge0div  9688  peano2uz2  9708  peano5uzti  9709  eluzp1m1  9901  xleadd1a  10230  iooshf  10309  divelunit  10359  eluzgtdifelfzo  10569  zsupcllemex  10617  infssfzcldc  10623  infssfzledc  10624  ioom  10649  modqcyc2  10751  modaddmodup  10778  uzennn  10827  seq3fveq2  10866  seqfveq2g  10868  seq3id2  10917  seqfeq3  10920  expineg2  10939  mulexpzap  10970  leexp2r  10984  expnlbnd2  11057  hashmap  11222  sseqn  11233  hashfibclem  11236  hashfacen  11238  wrdred1hash  11298  ccatsymb  11320  swrdwrdsymbg  11386  swrdsb0eq  11387  ccatpfx  11423  swrdswrd  11427  wrdind  11444  wrd2ind  11445  swrdccatin1  11447  swrdccatin2  11451  pfxccatin12lem2  11453  pfxccatin12  11455  pfxccat3  11456  swrdccat  11457  resqrexlemp1rp  11722  resqrexlemfp1  11725  negfi  11944  climcaucn  12067  fsum3cvg3  12113  fsum2dlemstep  12151  mptfzshft  12159  expcnvre  12220  fprodrev  12336  fprod2dlemstep  12339  moddvds  12516  dvdsflip  12568  addmodlteqALT  12576  nn0o  12624  dfgcd2  12741  lcmgcdlem  12805  cncongr1  12831  prmind2  12848  isprm5lem  12869  isprm6  12875  cncongrprm  12885  oddpwdclemdc  12901  sqrt2irrap  12908  hashdvds  12949  crth  12952  prmdiveq  12964  hashgcdlem  12966  hashgcdeq  12968  pclem0  13015  pclemub  13016  pcprendvds2  13020  pcmul  13030  pcexp  13038  pcneg  13054  pc2dvds  13059  pcmpt  13072  prmpwdvds  13084  pockthg  13086  1arith  13096  4sqlem2  13118  4sqlemafi  13124  4sqlem11  13130  ballotfilemsf1o  13207  ennnfonelemex  13255  setscom  13342  subsubm  13744  insubm  13746  isgrpinv  13815  subsubg  13956  subsubrng  14466  subsubrg  14497  islss4  14662  znf1o  14931  znidomb  14938  tgcl  15061  lmbr2  15211  txcn  15272  txdis1cn  15275  txlm  15276  hmeoimaf1o  15311  txhmeo  15316  bl2in  15400  blssps  15424  blss  15425  blssexps  15426  blssex  15427  bdxmet  15498  xmetxp  15504  xmetxpbl  15505  xmettx  15507  metcnp3  15508  metcnpi3  15514  dedekindicc  15630  ivthdichlem  15648  limcimolemlt  15661  dvmptfsum  15722  rprelogbmul  15952  logbgcd1irr  15964  mpodvdsmulf1o  15990  lgsne0  16043  gausslemma2dlem1a  16063  lgseisenlem2  16076  lgsquadlemsfi  16080  lgsquadlem1  16082  lgsquadlem2  16083  lgsquadlem3  16084  lgsquad2lem2  16087  2sqlem8  16128  uspgredg2vlem  16347  subuhgr  16399  subupgr  16400  subumgr  16401  iswlkg  16456  wlkl1loop  16485  upgriswlkdc  16487  clwwlkccatlem  16527  clwwlkn1loopb  16547  clwwlknonex2e  16567  qdencn  16949  trilpolemlt1  16967