Theorem 3adant2 1016

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

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

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 980

This theorem is referenced by:  3ad2ant1  1018  3imp3i2an  1183  eupickb  2107  vtoclegft  2809  eqeu  2907  suc11g  4554  soinxp  4694  funopg  5247  fnco  5321  dff1o2  5463  fnimapr  5573  fvun1  5579  fvmptt  5604  fnreseql  5623  fvpr1g  5719  fvpr2g  5720  f1elima  5769  f1ocnvfvb  5776  ovexg  5904  oprssov  6011  poxp  6228  smoiso  6298  rdgivallem  6377  nndi  6482  nndir  6486  fnsnsplitdc  6501  nnaord  6505  nnaordr  6506  nnaword  6507  nnawordi  6511  ecopovtrn  6627  ecopovtrng  6630  xpdom3m  6829  mapxpen  6843  findcard  6883  fisseneq  6926  resfnfinfinss  6934  funrnfi  6936  netap  7248  2omotaplemap  7251  ltsopi  7314  addcanpig  7328  addassnqg  7376  distrnqg  7381  ltsonq  7392  ltmnqg  7395  prarloclemarch2  7413  nnanq0  7452  distrnq0  7453  distnq0r  7457  prltlu  7481  prarloclem5  7494  distrlem1prl  7576  distrlem1pru  7577  distrlem5prl  7580  distrlem5pru  7581  ltpopr  7589  ltsopr  7590  ltexprlemm  7594  ltexprlemfl  7603  ltexprlemfu  7605  lttrsr  7756  ltsosr  7758  ltasrg  7764  recexgt0sr  7767  mulextsr1lem  7774  mulextsr1  7775  axpre-mulext  7882  adddir  7943  axltwlin  8019  axlttrn  8020  ltleletr  8033  letr  8034  nnncan1  8187  npncan3  8189  pnpcan2  8191  subdi  8336  subdir  8337  reapcotr  8549  divmulap  8626  div23ap  8642  div13ap  8644  muldivdirap  8658  divsubdirap  8659  divcanap7  8672  ltmul2  8807  lemul2  8808  lemul2a  8810  lediv1  8820  ltmuldiv2  8826  lemuldiv2  8833  squeeze0  8855  nndivtr  8955  bndndx  9169  nn0n0n1ge2  9317  fnn0ind  9363  addlelt  9762  xrletr  9802  xrltne  9807  xleadd2a  9868  xleadd1  9869  xltadd2  9871  iooneg  9982  iccneg  9983  icoshft  9984  icoshftf1o  9985  zltaddlt1le  10001  fztri3or  10032  fzdcel  10033  fzen  10036  uzsubsubfz  10040  fzrevral2  10099  fzshftral  10101  fz0fzdiffz0  10123  elfzmlbp  10125  elfzo  10142  fzoaddel2  10186  fzosubel2  10188  elfzom1p1elfzo  10207  ssfzo12bi  10218  subfzo0  10235  flltdivnn0lt  10297  modqmulnn  10335  modfzo0difsn  10388  expdivap  10564  expubnd  10570  mulbinom2  10629  bernneq2  10634  shftuz  10817  shftval2  10826  abs3dif  11105  xrmaxlesup  11258  xrltmininf  11269  xrlemininf  11270  sin02gt0  11762  dvdsval2  11788  dvdscmul  11816  dvdsmulc  11817  ndvdssub  11925  rpmulgcd  12017  cncongr1  12093  cncongr2  12094  isprm3  12108  coprimeprodsq  12247  pythagtriplem12  12265  pythagtriplem14  12267  pcmul  12291  pcdiv  12292  pcqcl  12296  pcqdiv  12297  pcdvdsb  12309  mgmb1mgm1  12717  grpinvid1  12852  grpinvid2  12853  grpasscan1  12861  grpasscan2  12862  grpinvadd  12876  grpsubf  12877  grpsubrcan  12879  grpinvsub  12880  grpsubeq0  12884  grpsubadd0sub  12885  grppncan  12889  grpnpcan  12890  mulgnn0p1  12922  mulgaddcomlem  12933  mulginvcom  12935  mulginvinv  12936  subgsubcl  12971  subgsub  12972  subcmnd  13029  srg1zr  13070  dvrcl  13203  unitdvcl  13204  dvrcan1  13208  dvrcan3  13209  dvreq1  13210  ntrin  13406  elnei  13434  cnrest2  13518  psmetsym  13611  psmetge0  13613  xmetge0  13647  xmetsym  13650  cnmet  13812  rpcxpsub  14111  rpdivcxp  14114  logbleb  14161  logblt  14162  lgsmodeq  14228  lgsmulsqcoprm  14229  bj-peano4  14478