Theorem 3ad2ant1 1020

Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)

Hypothesis

Ref	Expression
3ad2ant.1	⊢ (𝜑 → 𝜒)

Assertion

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

Proof of Theorem 3ad2ant1

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  simp1l  1023  simp1r  1024  simp11  1029  simp12  1030  simp13  1031  simp1ll  1062  simp1lr  1063  simp1rl  1064  simp1rr  1065  simp1l1  1092  simp1l2  1093  simp1l3  1094  simp1r1  1095  simp1r2  1096  simp1r3  1097  simp11l  1110  simp11r  1111  simp12l  1112  simp12r  1113  simp13l  1114  simp13r  1115  simp111  1128  simp112  1129  simp113  1130  simp121  1131  simp122  1132  simp123  1133  simp131  1134  simp132  1135  simp133  1136  3anim123i  1186  3jaao  1320  ceqsalt  2797  sbciegft  3028  reupick2  3458  ifbothdc  3604  frirrg  4396  breldmg  4883  fntpg  5329  funimaexglem  5356  fex2  5443  fvun1  5644  fprg  5766  fsnunfv  5784  fnfvima  5818  cocan1  5855  cocan2  5856  mpoeq3dv  6010  fovcld  6049  fvmpopr2d  6081  funexw  6196  mpofvex  6290  poxp  6317  smoiso  6387  tfrlem5  6399  tfrlemibxssdm  6412  tfr1onlembfn  6429  tfri1dALT  6436  tfrcllembfn  6442  rdgon  6471  freccllem  6487  nnawordex  6614  mapxpen  6944  fidceq  6965  fidifsnen  6966  dif1en  6975  en2eqpr  7003  unsnfi  7015  unsnfidcex  7016  unsnfidcel  7017  fisseneq  7030  ordiso2  7136  updjud  7183  mkvprop  7259  endjudisj  7321  xpdjuen  7329  mulcanenq0ec  7557  prltlu  7599  prarloclem3step  7608  prarloclem5  7612  ltasrg  7882  cnegexlem1  8246  addcan  8251  apcotr  8679  apadd1  8680  mulext1  8684  divdivap1  8795  divdivap2  8796  div2negap  8807  divneg2ap  8808  ltmulgt11  8936  ltdiv2  8959  squeeze0  8976  nndivtr  9077  nn0n0n1ge2  9442  zdivmul  9462  gtndiv  9467  eluzuzle  9655  eluzp1p1  9673  qdivcl  9763  irrmul  9767  rpgecl  9803  xaddass  9990  xltadd1  9997  xlt2add  10001  lbico1  10051  lbicc2  10105  zltaddlt1le  10128  uzsubsubfz  10168  elfz1b  10211  elfz0ubfz0  10246  fz0fzelfz0  10248  difelfzle  10255  difelfznle  10256  2ffzeq  10262  fzo1fzo0n0  10305  ubmelfzo  10327  fzonn0p1p1  10340  elfzom1p1elfzo  10341  elfzonelfzo  10357  subfzo0  10369  ceiqle  10456  ceilqle  10457  modqval  10467  flqpmodeq  10470  modq0  10472  negqmod0  10474  modqge0  10475  modqlt  10476  modqdiffl  10478  modqmulnn  10485  modqvalp1  10486  modqmuladdnn0  10511  qnegmod  10512  addmodid  10515  modfzo0difsn  10538  addmodlteq  10541  qexpclz  10703  expgt1  10720  expp1zap  10731  expm1ap  10732  expubnd  10739  bernneq2  10804  expnlbnd  10807  mulsubdivbinom2ap  10854  omgadd  10945  hashun  10948  fihashssdif  10961  hashdifpr  10963  fimaxq  10970  ccatval2  11052  ccatval3  11053  ccatval1lsw  11058  ccatval21sw  11059  ccatass  11062  ccats1val2  11090  shftuz  11099  mulreap  11146  redivap  11156  imdivap  11163  resqrtcl  11311  xrmaxltsup  11540  xrmaxaddlem  11542  xrmaxadd  11543  xrlemininf  11553  xrminltinf  11554  climuni  11575  addcn2  11592  mulcn2  11594  efsub  11963  sin02gt0  12046  cos12dec  12050  dvdsval2  12072  addmodlteqALT  12141  modremain  12211  fldivndvdslt  12219  mulgcdr  12310  gcddiv  12311  rpmulgcd  12318  rplpwr  12319  rppwr  12320  nnminle  12327  qredeq  12389  divgcdcoprmex  12395  cncongr1  12396  cncongr2  12397  dvdsnprmd  12418  euclemma  12439  prmexpb  12444  qnumdenbi  12485  eulerth  12526  fermltl  12527  prmdiv  12528  hashgcdlem  12531  odzcllem  12536  vfermltl  12545  reumodprminv  12547  modprm0  12548  modprmn0modprm0  12550  coprimeprodsq  12551  pythagtriplem1  12559  pythagtriplem3  12561  pythagtriplem4  12562  pythagtriplem10  12563  pythagtriplem6  12564  pythagtriplem7  12565  pythagtriplem8  12566  pythagtriplem9  12567  pythagtriplem11  12568  pythagtriplem12  12569  pythagtriplem13  12570  pythagtriplem14  12571  pythagtriplem15  12572  pythagtriplem16  12573  pythagtriplem17  12574  pythagtriplem19  12576  pythagtrip  12577  pcpremul  12587  pcdvdsb  12614  dvdsprmpweqnn  12630  dvdsprmpweqle  12631  difsqpwdvds  12632  pcfaclem  12643  pcbc  12645  4sqlem12  12696  unennn  12739  nninfdc  12795  setsex  12835  f1ocpbllem  13113  imasaddfnlemg  13117  imasaddvallemg  13118  ercpbl  13134  erlecpbl  13135  qusaddvallemg  13136  fvprif  13146  xpsfrnel2  13149  plusfvalg  13166  imasmnd  13256  insubm  13288  grpidrcan  13368  grpidlcan  13369  grpsubpropd2  13408  pwsinvg  13415  imasgrp2  13417  imasgrp  13418  mulgnnsubcl  13441  mulgnn0subcl  13442  mulgsubcl  13443  mulgaddcom  13453  mulginvcom  13454  mulgnnass  13464  mulgassr  13467  mulgpropdg  13471  submmulg  13473  subgcl  13491  subgsubcl  13492  subgsub  13493  subgmulg  13495  nsgconj  13513  ghmsub  13558  ghmrn  13564  ghmeqker  13578  f1ghm0to0  13579  ablinvadd  13617  ablsub4  13620  abladdsub4  13621  subcmnd  13640  imasabl  13643  rngcl  13677  imasrng  13689  srgcl  13703  srg1zr  13720  srgen1zr  13721  ringcl  13746  crngcom  13747  ringidss  13762  mulgass2  13791  imasring  13797  opprmulg  13804  unitmulclb  13847  unitdvcl  13869  rhmmul  13897  rhmdvdsr  13908  subrngmcl  13942  subrgmcl  13966  subrgdv  13971  subrgugrp  13973  domneq0  14005  scafvalg  14040  lmodprop2d  14081  lssclg  14097  lssvnegcl  14109  lssintclm  14117  sralmod  14183  rnglidlmcl  14213  lidlnegcl  14218  rspssp  14227  rnglidlmsgrp  14230  rnglidlrng  14231  2idlcpblrng  14256  qus2idrng  14258  zndvds  14382  znleval2  14387  basgen  14523  2basgeng  14525  iuncld  14558  neipsm  14597  opnneissb  14598  opnssneib  14599  iscnp3  14646  cnprcl2k  14649  cnpnei  14662  cncnp2m  14674  cnptoprest  14682  sslm  14690  upxp  14715  cnmpt22  14737  distspace  14778  0met  14827  blvalps  14831  blval  14832  ssblps  14868  ssbl  14869  blpnfctr  14882  blopn  14933  blnei  14935  bdxmet  14944  bdbl  14946  metcnp3  14954  tgqioo  14998  ptolemy  15267  sinq12gt0  15273  sincosq1eq  15282  rpcxpadd  15348  cxpmul  15355  rplogbval  15388  logbleb  15404  logbgcd1irr  15410  logbprmirr  15415  lgsfvalg  15453  lgsneg1  15473  lgssq  15488  lgsdinn0  15496  gausslemma2dlem1a  15506  2lgs  15552  2lgsoddprmlem2  15554  funvtxdm2domval  15597  funiedgdm2domval  15598  bdfind  15844  1dom1el  15889