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  1319  ceqsalt  2789  sbciegft  3020  reupick2  3450  ifbothdc  3595  frirrg  4386  breldmg  4873  fntpg  5315  funimaexglem  5342  fex2  5429  fvun1  5630  fprg  5748  fsnunfv  5766  fnfvima  5800  cocan1  5837  cocan2  5838  mpoeq3dv  5992  fovcld  6031  fvmpopr2d  6063  funexw  6178  mpofvex  6272  poxp  6299  smoiso  6369  tfrlem5  6381  tfrlemibxssdm  6394  tfr1onlembfn  6411  tfri1dALT  6418  tfrcllembfn  6424  rdgon  6453  freccllem  6469  nnawordex  6596  mapxpen  6918  fidceq  6939  fidifsnen  6940  dif1en  6949  en2eqpr  6977  unsnfi  6989  unsnfidcex  6990  unsnfidcel  6991  fisseneq  7004  ordiso2  7110  updjud  7157  mkvprop  7233  endjudisj  7295  xpdjuen  7303  mulcanenq0ec  7531  prltlu  7573  prarloclem3step  7582  prarloclem5  7586  ltasrg  7856  cnegexlem1  8220  addcan  8225  apcotr  8653  apadd1  8654  mulext1  8658  divdivap1  8769  divdivap2  8770  div2negap  8781  divneg2ap  8782  ltmulgt11  8910  ltdiv2  8933  squeeze0  8950  nndivtr  9051  nn0n0n1ge2  9415  zdivmul  9435  gtndiv  9440  eluzuzle  9628  eluzp1p1  9646  qdivcl  9736  irrmul  9740  rpgecl  9776  xaddass  9963  xltadd1  9970  xlt2add  9974  lbico1  10024  lbicc2  10078  zltaddlt1le  10101  uzsubsubfz  10141  elfz1b  10184  elfz0ubfz0  10219  fz0fzelfz0  10221  difelfzle  10228  difelfznle  10229  2ffzeq  10235  fzo1fzo0n0  10278  ubmelfzo  10295  fzonn0p1p1  10308  elfzom1p1elfzo  10309  elfzonelfzo  10325  subfzo0  10337  ceiqle  10424  ceilqle  10425  modqval  10435  flqpmodeq  10438  modq0  10440  negqmod0  10442  modqge0  10443  modqlt  10444  modqdiffl  10446  modqmulnn  10453  modqvalp1  10454  modqmuladdnn0  10479  qnegmod  10480  addmodid  10483  modfzo0difsn  10506  addmodlteq  10509  qexpclz  10671  expgt1  10688  expp1zap  10699  expm1ap  10700  expubnd  10707  bernneq2  10772  expnlbnd  10775  mulsubdivbinom2ap  10822  omgadd  10913  hashun  10916  fihashssdif  10929  hashdifpr  10931  fimaxq  10938  shftuz  11001  mulreap  11048  redivap  11058  imdivap  11065  resqrtcl  11213  xrmaxltsup  11442  xrmaxaddlem  11444  xrmaxadd  11445  xrlemininf  11455  xrminltinf  11456  climuni  11477  addcn2  11494  mulcn2  11496  efsub  11865  sin02gt0  11948  cos12dec  11952  dvdsval2  11974  addmodlteqALT  12043  modremain  12113  fldivndvdslt  12121  mulgcdr  12212  gcddiv  12213  rpmulgcd  12220  rplpwr  12221  rppwr  12222  nnminle  12229  qredeq  12291  divgcdcoprmex  12297  cncongr1  12298  cncongr2  12299  dvdsnprmd  12320  euclemma  12341  prmexpb  12346  qnumdenbi  12387  eulerth  12428  fermltl  12429  prmdiv  12430  hashgcdlem  12433  odzcllem  12438  vfermltl  12447  reumodprminv  12449  modprm0  12450  modprmn0modprm0  12452  coprimeprodsq  12453  pythagtriplem1  12461  pythagtriplem3  12463  pythagtriplem4  12464  pythagtriplem10  12465  pythagtriplem6  12466  pythagtriplem7  12467  pythagtriplem8  12468  pythagtriplem9  12469  pythagtriplem11  12470  pythagtriplem12  12471  pythagtriplem13  12472  pythagtriplem14  12473  pythagtriplem15  12474  pythagtriplem16  12475  pythagtriplem17  12476  pythagtriplem19  12478  pythagtrip  12479  pcpremul  12489  pcdvdsb  12516  dvdsprmpweqnn  12532  dvdsprmpweqle  12533  difsqpwdvds  12534  pcfaclem  12545  pcbc  12547  4sqlem12  12598  unennn  12641  nninfdc  12697  setsex  12737  f1ocpbllem  13014  imasaddfnlemg  13018  imasaddvallemg  13019  ercpbl  13035  erlecpbl  13036  qusaddvallemg  13037  fvprif  13047  xpsfrnel2  13050  plusfvalg  13067  imasmnd  13157  insubm  13189  grpidrcan  13269  grpidlcan  13270  grpsubpropd2  13309  pwsinvg  13316  imasgrp2  13318  imasgrp  13319  mulgnnsubcl  13342  mulgnn0subcl  13343  mulgsubcl  13344  mulgaddcom  13354  mulginvcom  13355  mulgnnass  13365  mulgassr  13368  mulgpropdg  13372  submmulg  13374  subgcl  13392  subgsubcl  13393  subgsub  13394  subgmulg  13396  nsgconj  13414  ghmsub  13459  ghmrn  13465  ghmeqker  13479  f1ghm0to0  13480  ablinvadd  13518  ablsub4  13521  abladdsub4  13522  subcmnd  13541  imasabl  13544  rngcl  13578  imasrng  13590  srgcl  13604  srg1zr  13621  srgen1zr  13622  ringcl  13647  crngcom  13648  ringidss  13663  mulgass2  13692  imasring  13698  opprmulg  13705  unitmulclb  13748  unitdvcl  13770  rhmmul  13798  rhmdvdsr  13809  subrngmcl  13843  subrgmcl  13867  subrgdv  13872  subrgugrp  13874  domneq0  13906  scafvalg  13941  lmodprop2d  13982  lssclg  13998  lssvnegcl  14010  lssintclm  14018  sralmod  14084  rnglidlmcl  14114  lidlnegcl  14119  rspssp  14128  rnglidlmsgrp  14131  rnglidlrng  14132  2idlcpblrng  14157  qus2idrng  14159  zndvds  14283  znleval2  14288  basgen  14424  2basgeng  14426  iuncld  14459  neipsm  14498  opnneissb  14499  opnssneib  14500  iscnp3  14547  cnprcl2k  14550  cnpnei  14563  cncnp2m  14575  cnptoprest  14583  sslm  14591  upxp  14616  cnmpt22  14638  distspace  14679  0met  14728  blvalps  14732  blval  14733  ssblps  14769  ssbl  14770  blpnfctr  14783  blopn  14834  blnei  14836  bdxmet  14845  bdbl  14847  metcnp3  14855  tgqioo  14899  ptolemy  15168  sinq12gt0  15174  sincosq1eq  15183  rpcxpadd  15249  cxpmul  15256  rplogbval  15289  logbleb  15305  logbgcd1irr  15311  logbprmirr  15316  lgsfvalg  15354  lgsneg1  15374  lgssq  15389  lgsdinn0  15397  gausslemma2dlem1a  15407  2lgs  15453  2lgsoddprmlem2  15455  bdfind  15700  1dom1el  15745