Theorem 3adant2 1019

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 998	. 2 ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → (𝜑 ∧ 𝜓))
2		3adant.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	syl 14	1 ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜒)

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

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 983

This theorem is referenced by:  3ad2ant1  1021  3imp3i2an  1186  eupickb  2136  vtoclegft  2847  eqeu  2945  ifnebibdc  3617  suc11g  4610  soinxp  4750  funopg  5311  fnco  5390  dff1o2  5536  fnimapr  5649  fvun1  5655  fvmptt  5681  fnreseql  5700  fvpr1g  5800  fvpr2g  5801  f1elima  5852  f1ocnvfvb  5859  ovexg  5988  oprssov  6098  poxp  6328  smoiso  6398  rdgivallem  6477  nndi  6582  nndir  6586  fnsnsplitdc  6601  nnaord  6605  nnaordr  6606  nnaword  6607  nnawordi  6611  ecopovtrn  6729  ecopovtrng  6732  xpdom3m  6941  mapxpen  6957  findcard  6997  fisseneq  7043  resfnfinfinss  7053  funrnfi  7056  netap  7379  2omotaplemap  7382  ltsopi  7446  addcanpig  7460  addassnqg  7508  distrnqg  7513  ltsonq  7524  ltmnqg  7527  prarloclemarch2  7545  nnanq0  7584  distrnq0  7585  distnq0r  7589  prltlu  7613  prarloclem5  7626  distrlem1prl  7708  distrlem1pru  7709  distrlem5prl  7712  distrlem5pru  7713  ltpopr  7721  ltsopr  7722  ltexprlemm  7726  ltexprlemfl  7735  ltexprlemfu  7737  lttrsr  7888  ltsosr  7890  ltasrg  7896  recexgt0sr  7899  mulextsr1lem  7906  mulextsr1  7907  axpre-mulext  8014  adddir  8076  axltwlin  8153  axlttrn  8154  ltleletr  8167  letr  8168  nnncan1  8321  npncan3  8323  pnpcan2  8325  subdi  8470  subdir  8471  reapcotr  8684  divmulap  8761  div23ap  8777  div13ap  8779  muldivdirap  8793  divsubdirap  8794  divcanap7  8807  ltmul2  8942  lemul2  8943  lemul2a  8945  lediv1  8955  ltmuldiv2  8961  lemuldiv2  8968  squeeze0  8990  nndivtr  9091  bndndx  9307  nn0n0n1ge2  9456  fnn0ind  9502  addlelt  9903  xrletr  9943  xrltne  9948  xleadd2a  10009  xleadd1  10010  xltadd2  10012  iooneg  10123  iccneg  10124  icoshft  10125  icoshftf1o  10126  zltaddlt1le  10142  fztri3or  10174  fzdcel  10175  fzen  10178  uzsubsubfz  10182  fzrevral2  10241  fzshftral  10243  fz0fzdiffz0  10265  elfzmlbp  10267  elfzo  10284  nelfzo  10287  fzoaddel2  10332  fzosubel2  10337  elfzom1p1elfzo  10356  ssfzo12bi  10367  subfzo0  10384  flltdivnn0lt  10460  modqmulnn  10500  modfzo0difsn  10553  expdivap  10748  expubnd  10754  mulbinom2  10814  bernneq2  10819  ccatval1  11067  ccatval3  11069  ccatfv0  11073  ccatval1lsw  11074  ccatws1lenp1bg  11103  pfxsuffeqwrdeq  11163  pfxsuff1eqwrdeq  11164  swrdswrd  11170  pfxpfx  11173  shftuz  11178  shftval2  11187  abs3dif  11466  xrmaxlesup  11620  xrltmininf  11631  xrlemininf  11632  sin02gt0  12125  dvdsval2  12151  dvdscmul  12179  dvdsmulc  12180  ndvdssub  12291  rpmulgcd  12397  cncongr1  12475  cncongr2  12476  isprm3  12490  coprimeprodsq  12630  pythagtriplem12  12648  pythagtriplem14  12650  pcmul  12674  pcdiv  12675  pcqcl  12679  pcqdiv  12680  pcdvdsb  12693  ercpbl  13213  mgmb1mgm1  13250  grpinvid1  13434  grpinvid2  13435  grpasscan1  13445  grpasscan2  13446  grpinvadd  13460  grpsubf  13461  grpsubrcan  13463  grpinvsub  13464  grpsubeq0  13468  grpsubadd0sub  13469  grppncan  13473  grpnpcan  13474  mulgnn0p1  13519  mulgaddcomlem  13531  mulginvcom  13533  mulginvinv  13534  subgsubcl  13571  subgsub  13572  eqglact  13611  quselbasg  13616  quseccl0g  13617  qussub  13623  ghmsub  13637  subcmnd  13719  srg1zr  13799  dvrcl  13947  unitdvcl  13948  dvrcan1  13952  dvrcan3  13953  dvreq1  13954  subrgdv  14050  lmodvsubval2  14154  lmodprop2d  14160  zndvds  14461  ntrin  14646  elnei  14674  cnrest2  14758  psmetsym  14851  psmetge0  14853  xmetge0  14887  xmetsym  14890  cnmet  15052  rpcxpsub  15430  rpdivcxp  15433  logbleb  15483  logblt  15484  lgsmodeq  15572  lgsmulsqcoprm  15573  gausslemma2dlem1a  15585  2lgsoddprmlem2  15633  bj-peano4  16005