Theorem 3adant3 1001

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)

Hypothesis

Ref	Expression
3adant.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
3adant3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

Proof of Theorem 3adant3

Step	Hyp	Ref	Expression
1		3simpa 978	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → (𝜑 ∧ 𝜓))
2		3adant.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	syl 14	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  stoic4a  1408  stoic4b  1409  vtoclgft  2736  eqeu  2854  tpssi  3686  issod  4241  sotricim  4245  soinxp  4609  funopg  5157  fnco  5231  resasplitss  5302  resdif  5389  fnimapr  5481  ftpg  5604  fsnunfv  5621  fvpr1g  5626  fvpr2g  5627  f1ocnvfvb  5681  f1oiso2  5728  moriotass  5758  f1ofveu  5762  acexmid  5773  ovig  5892  ov6g  5908  ovg  5909  ot1stg  6050  ot2ndg  6051  poxp  6129  brtposg  6151  smores3  6190  smoiso  6199  rdgivallem  6278  frecsuclem  6303  nnaord  6405  nnaword  6407  nnawordex  6424  ecopovtrn  6526  ecopovtrng  6529  xpdom3m  6728  mapxpen  6742  sbthlemi4  6848  djuenun  7068  ltsopi  7128  addcanpig  7142  distrnqg  7195  ltsonq  7206  ltanqg  7208  ltmnqg  7209  nnanq0  7266  distrnq0  7267  distnq0r  7271  prarloclem  7309  genpassl  7332  genpassu  7333  distrlem1prl  7390  distrlem1pru  7391  distrlem5prl  7394  distrlem5pru  7395  1idprl  7398  1idpru  7399  ltpopr  7403  ltsopr  7404  ltexprlemm  7408  ltexprlemfl  7417  ltexprlemfu  7419  addcanprlemu  7423  recexprlem1ssl  7441  recexprlem1ssu  7442  aptipr  7449  lttrsr  7570  ltsosr  7572  ltasrg  7578  recexgt0sr  7581  mulextsr1  7589  axmulass  7681  ltxrlt  7830  axltwlin  7832  axlttrn  7833  axltadd  7834  letr  7847  mul12  7891  add12  7920  subadd  7965  addsub  7973  npncan  7983  nppcan  7984  nnpcan  7985  nppcan3  7986  pnpcan  8001  pnncan  8003  ppncan  8004  subdi  8147  ltaddsub2  8199  leaddsub2  8201  ltaddsublt  8333  apreap  8349  lemul1  8355  reapmul1lem  8356  reapadd1  8358  reapcotr  8360  receuap  8430  divassap  8450  div23ap  8451  divmulassap  8455  divmulasscomap  8456  divcanap4  8459  divsubdirap  8468  divcanap5  8474  divdiv32ap  8480  divdivap2  8484  div2subap  8596  letrp1  8606  ltmulgt12  8623  lediv1  8627  ltdiv2  8645  lediv2  8649  lbinfle  8708  xrletr  9591  xrre2  9604  xaddass  9652  ixxdisj  9686  ubioc1  9712  lbico1  9713  elioo5  9716  iccsupr  9749  lbicc2  9767  ubicc2  9768  iccneg  9772  icoshft  9773  icodisj  9775  iccf1o  9787  zltaddlt1le  9789  fztri3or  9819  fzdcel  9820  fzen  9823  uzsubsubfz  9827  fzrevral2  9886  fzshftral  9888  fz0fzdiffz0  9907  difelfznle  9912  fzo1fzo0n0  9960  fzonmapblen  9964  fzosubel2  9972  ubmelfzo  9977  elfzodifsumelfzo  9978  ssfzo12bi  10002  ubmelm1fzo  10003  subfzo0  10019  ceiqle  10086  modqid2  10124  zmodidfzoimp  10127  addmodidr  10146  modfzo0difsn  10168  addmodlteq  10171  frec2uzf1od  10179  exprecap  10334  expdivap  10344  expubnd  10350  sqdivap  10357  mulbinom2  10408  bernneq2  10413  bcval3  10497  bccmpl  10500  omgadd  10548  shftval2  10598  mulreap  10636  elicc4abs  10866  abssubge0  10874  abssuble0  10875  maxleast  10985  maxltsup  10990  xrmaxltsup  11027  xrmineqinf  11038  xrltmininf  11039  xrlemininf  11040  fsumdifsnconst  11224  prodfap0  11314  prodfrecap  11315  sin01gt0  11468  cos01gt0  11469  sin02gt0  11470  dvdscmul  11520  summodnegmod  11524  modmulconst  11525  dvdsleabs  11543  dvdsleabs2  11544  addmodlteqALT  11557  dvdsexp  11559  mulmoddvds  11561  divalgb  11622  divgcdz  11660  gcdass  11703  mulgcdr  11706  gcddiv  11707  lcmass  11766  coprmdvds  11773  qredeq  11777  qredeu  11778  congr  11781  divgcdcoprm0  11782  divgcdcoprmex  11783  cncongr1  11784  cncongr2  11785  isprm3  11799  dvdsnprmd  11806  euclemma  11824  prmdvdsexpb  11827  prmexpb  11829  rpexp  11831  znege1  11856  strle3g  12051  basgen  12249  clsss  12287  ntrin  12293  ntrcls0  12300  neiint  12314  neiss  12319  neipsm  12323  opnssneib  12325  innei  12332  restco  12343  iscnp  12368  cnconst2  12402  txcn  12444  psmetsym  12498  psmetlecl  12503  distspace  12504  xmetlecl  12536  xmetsym  12537  xblcntrps  12582  xblcntr  12583  blssec  12607  blpnfctr  12608  txmetcn  12688  cnmet  12699  dvid  12831  ptolemy  12905  sinq12gt0  12911  sincosq1eq  12920