Theorem 3adant2 1043

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

Hypothesis

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

Assertion

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

Proof of Theorem 3adant2

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1005

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 depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  3ad2ant1  1045  3imp3i2an  1210  eupickb  2161  vtoclegft  2879  eqeu  2977  ifnebibdc  3655  suc11g  4661  soinxp  4802  funopg  5367  fnco  5447  dff1o2  5597  fnimapr  5715  fvun1  5721  fvmptt  5747  fnreseql  5766  fvpr1g  5868  fvpr2g  5869  f1elima  5924  f1ocnvfvb  5931  ovexg  6062  oprssov  6174  poxp  6406  smoiso  6511  rdgivallem  6590  nndi  6697  nndir  6701  fnsnsplitdc  6716  nnaord  6720  nnaordr  6721  nnaword  6722  nnawordi  6726  ecopovtrn  6844  ecopovtrng  6847  xpdom3m  7061  mapxpen  7077  findcard  7120  fisseneq  7170  resfnfinfinss  7181  funrnfi  7184  netap  7516  2omotaplemap  7519  ltsopi  7583  addcanpig  7597  addassnqg  7645  distrnqg  7650  ltsonq  7661  ltmnqg  7664  prarloclemarch2  7682  nnanq0  7721  distrnq0  7722  distnq0r  7726  prltlu  7750  prarloclem5  7763  distrlem1prl  7845  distrlem1pru  7846  distrlem5prl  7849  distrlem5pru  7850  ltpopr  7858  ltsopr  7859  ltexprlemm  7863  ltexprlemfl  7872  ltexprlemfu  7874  lttrsr  8025  ltsosr  8027  ltasrg  8033  recexgt0sr  8036  mulextsr1lem  8043  mulextsr1  8044  axpre-mulext  8151  adddir  8213  axltwlin  8290  axlttrn  8291  ltleletr  8304  letr  8305  nnncan1  8458  npncan3  8460  pnpcan2  8462  subdi  8607  subdir  8608  reapcotr  8821  divmulap  8898  div23ap  8914  div13ap  8916  muldivdirap  8930  divsubdirap  8931  divcanap7  8944  ltmul2  9079  lemul2  9080  lemul2a  9082  lediv1  9092  ltmuldiv2  9098  lemuldiv2  9105  squeeze0  9127  nndivtr  9228  bndndx  9444  nn0n0n1ge2  9593  fnn0ind  9639  addlelt  10046  xrletr  10086  xrltne  10091  xleadd2a  10152  xleadd1  10153  xltadd2  10155  iooneg  10266  iccneg  10267  icoshft  10268  icoshftf1o  10269  zltaddlt1le  10285  fztri3or  10317  fzdcel  10318  fzen  10321  uzsubsubfz  10325  fzrevral2  10384  fzshftral  10386  fz0fzdiffz0  10408  elfzmlbp  10410  elfzo  10427  nelfzo  10430  fzoaddel2  10479  fzosubel2  10484  elfzom1p1elfzo  10503  ssfzo12bi  10514  subfzo0  10532  flltdivnn0lt  10608  modqmulnn  10648  modfzo0difsn  10701  expdivap  10896  expubnd  10902  mulbinom2  10962  bernneq2  10967  ccatval1  11221  ccatval3  11223  ccatfv0  11227  ccatval1lsw  11228  ccatws1lenp1bg  11259  pfxsuffeqwrdeq  11326  pfxsuff1eqwrdeq  11327  swrdswrd  11333  pfxpfx  11336  wrd2ind  11351  swrdccatin1  11353  pfxccatin12lem1  11356  swrdccatin2  11357  pfxccatin12lem3  11360  swrdccat  11363  pfxccatpfx1  11364  pfxccatpfx2  11365  swrdccat3blem  11367  shftuz  11438  shftval2  11447  abs3dif  11726  xrmaxlesup  11880  xrltmininf  11891  xrlemininf  11892  sin02gt0  12386  dvdsval2  12412  dvdscmul  12440  dvdsmulc  12441  ndvdssub  12552  rpmulgcd  12658  cncongr1  12736  cncongr2  12737  isprm3  12751  coprimeprodsq  12891  pythagtriplem12  12909  pythagtriplem14  12911  pcmul  12935  pcdiv  12936  pcqcl  12940  pcqdiv  12941  pcdvdsb  12954  ercpbl  13475  mgmb1mgm1  13512  grpinvid1  13696  grpinvid2  13697  grpasscan1  13707  grpasscan2  13708  grpinvadd  13722  grpsubf  13723  grpsubrcan  13725  grpinvsub  13726  grpsubeq0  13730  grpsubadd0sub  13731  grppncan  13735  grpnpcan  13736  mulgnn0p1  13781  mulgaddcomlem  13793  mulginvcom  13795  mulginvinv  13796  subgsubcl  13833  subgsub  13834  eqglact  13873  quselbasg  13878  quseccl0g  13879  qussub  13885  ghmsub  13899  subcmnd  13981  srg1zr  14062  dvrcl  14211  unitdvcl  14212  dvrcan1  14216  dvrcan3  14217  dvreq1  14218  subrgdv  14314  lmodvsubval2  14418  lmodprop2d  14424  zndvds  14725  ntrin  14915  elnei  14943  cnrest2  15027  psmetsym  15120  psmetge0  15122  xmetge0  15156  xmetsym  15159  cnmet  15321  rpcxpsub  15699  rpdivcxp  15702  logbleb  15752  logblt  15753  lgsmodeq  15844  lgsmulsqcoprm  15845  gausslemma2dlem1a  15857  2lgsoddprmlem2  15905  upgrpredgv  16067  issubgr2  16179  uhgrissubgr  16182  egrsubgr  16184  upgrwlkvtxedg  16285  clwwlk1loop  16320  clwwlkccatlem  16321  clwwlknonex2lem2  16359  bj-peano4  16651