Theorem 3ad2ant1 1042

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 1040	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  simp1l  1045  simp1r  1046  simp11  1051  simp12  1052  simp13  1053  simp1ll  1084  simp1lr  1085  simp1rl  1086  simp1rr  1087  simp1l1  1114  simp1l2  1115  simp1l3  1116  simp1r1  1117  simp1r2  1118  simp1r3  1119  simp11l  1132  simp11r  1133  simp12l  1134  simp12r  1135  simp13l  1136  simp13r  1137  simp111  1150  simp112  1151  simp113  1152  simp121  1153  simp122  1154  simp123  1155  simp131  1156  simp132  1157  simp133  1158  3anim123i  1208  3jaao  1342  ceqsalt  2826  sbciegft  3059  reupick2  3490  ifbothdc  3637  frirrg  4441  breldmg  4929  fntpg  5377  funimaexglem  5404  fex2  5494  fvun1  5702  fprg  5826  fsnunfv  5844  fnfvima  5878  cocan1  5917  cocan2  5918  mpoeq3dv  6076  fovcld  6115  fvmpopr2d  6147  funexw  6263  mpofvex  6357  poxp  6384  smoiso  6454  tfrlem5  6466  tfrlemibxssdm  6479  tfr1onlembfn  6496  tfri1dALT  6503  tfrcllembfn  6509  rdgon  6538  freccllem  6554  nnawordex  6683  mapxpen  7017  fidceq  7039  fidifsnen  7040  dif1en  7049  en2eqpr  7080  unsnfi  7092  unsnfidcex  7093  unsnfidcel  7094  fisseneq  7107  ordiso2  7213  updjud  7260  mkvprop  7336  endjudisj  7403  xpdjuen  7411  mulcanenq0ec  7643  prltlu  7685  prarloclem3step  7694  prarloclem5  7698  ltasrg  7968  cnegexlem1  8332  addcan  8337  apcotr  8765  apadd1  8766  mulext1  8770  divdivap1  8881  divdivap2  8882  div2negap  8893  divneg2ap  8894  ltmulgt11  9022  ltdiv2  9045  squeeze0  9062  nndivtr  9163  nn0n0n1ge2  9528  zdivmul  9548  gtndiv  9553  eluzuzle  9742  eluzp1p1  9760  qdivcl  9850  irrmul  9854  rpgecl  9890  xaddass  10077  xltadd1  10084  xlt2add  10088  lbico1  10138  lbicc2  10192  zltaddlt1le  10215  uzsubsubfz  10255  elfz1b  10298  elfz0ubfz0  10333  fz0fzelfz0  10335  difelfzle  10342  difelfznle  10343  2ffzeq  10349  fzo1fzo0n0  10395  ubmelfzo  10418  fzonn0p1p1  10431  elfzom1p1elfzo  10432  elfzonelfzo  10448  subfzo0  10460  ceiqle  10547  ceilqle  10548  modqval  10558  flqpmodeq  10561  modq0  10563  negqmod0  10565  modqge0  10566  modqlt  10567  modqdiffl  10569  modqmulnn  10576  modqvalp1  10577  modqmuladdnn0  10602  qnegmod  10603  addmodid  10606  modfzo0difsn  10629  addmodlteq  10632  qexpclz  10794  expgt1  10811  expp1zap  10822  expm1ap  10823  expubnd  10830  bernneq2  10895  expnlbnd  10898  mulsubdivbinom2ap  10945  omgadd  11036  hashun  11039  fihashssdif  11053  hashdifpr  11055  fimaxq  11062  ccatval2  11146  ccatval3  11147  ccatval1lsw  11152  ccatval21sw  11153  ccatass  11156  ccats1val2  11186  fzowrddc  11194  swrdval  11195  swrdclg  11197  swrdval2  11198  swrdnd  11206  swrdlen2  11209  swrdfv2  11210  ccatswrd  11217  pfxn0  11235  pfxsuff1eqwrdeq  11246  swrdswrdlem  11251  ccats1pfxeq  11261  ccats1pfxeqrex  11262  ccatopth2  11264  wrd2ind  11270  pfxccatin12lem3  11279  pfxccat3  11281  swrdccat  11282  pfxccatpfx2  11284  pfxccat3a  11285  swrdccat3b  11287  pfxccatid  11288  ccats1pfxeqbi  11289  shftuz  11343  mulreap  11390  redivap  11400  imdivap  11407  resqrtcl  11555  xrmaxltsup  11784  xrmaxaddlem  11786  xrmaxadd  11787  xrlemininf  11797  xrminltinf  11798  climuni  11819  addcn2  11836  mulcn2  11838  efsub  12207  sin02gt0  12290  cos12dec  12294  dvdsval2  12316  addmodlteqALT  12385  modremain  12455  fldivndvdslt  12463  mulgcdr  12554  gcddiv  12555  rpmulgcd  12562  rplpwr  12563  rppwr  12564  nnminle  12571  qredeq  12633  divgcdcoprmex  12639  cncongr1  12640  cncongr2  12641  dvdsnprmd  12662  euclemma  12683  prmexpb  12688  qnumdenbi  12729  eulerth  12770  fermltl  12771  prmdiv  12772  hashgcdlem  12775  odzcllem  12780  vfermltl  12789  reumodprminv  12791  modprm0  12792  modprmn0modprm0  12794  coprimeprodsq  12795  pythagtriplem1  12803  pythagtriplem3  12805  pythagtriplem4  12806  pythagtriplem10  12807  pythagtriplem6  12808  pythagtriplem7  12809  pythagtriplem8  12810  pythagtriplem9  12811  pythagtriplem11  12812  pythagtriplem12  12813  pythagtriplem13  12814  pythagtriplem14  12815  pythagtriplem15  12816  pythagtriplem16  12817  pythagtriplem17  12818  pythagtriplem19  12820  pythagtrip  12821  pcpremul  12831  pcdvdsb  12858  dvdsprmpweqnn  12874  dvdsprmpweqle  12875  difsqpwdvds  12876  pcfaclem  12887  pcbc  12889  4sqlem12  12940  unennn  12983  nninfdc  13039  setsex  13079  f1ocpbllem  13358  imasaddfnlemg  13362  imasaddvallemg  13363  ercpbl  13379  erlecpbl  13380  qusaddvallemg  13381  fvprif  13391  xpsfrnel2  13394  plusfvalg  13411  imasmnd  13501  insubm  13533  grpidrcan  13613  grpidlcan  13614  grpsubpropd2  13653  pwsinvg  13660  imasgrp2  13662  imasgrp  13663  mulgnnsubcl  13686  mulgnn0subcl  13687  mulgsubcl  13688  mulgaddcom  13698  mulginvcom  13699  mulgnnass  13709  mulgassr  13712  mulgpropdg  13716  submmulg  13718  subgcl  13736  subgsubcl  13737  subgsub  13738  subgmulg  13740  nsgconj  13758  ghmsub  13803  ghmrn  13809  ghmeqker  13823  f1ghm0to0  13824  ablinvadd  13862  ablsub4  13865  abladdsub4  13866  subcmnd  13885  imasabl  13888  rngcl  13922  imasrng  13934  srgcl  13948  srg1zr  13965  srgen1zr  13966  ringcl  13991  crngcom  13992  ringidss  14007  mulgass2  14036  imasring  14042  opprmulg  14049  unitmulclb  14093  unitdvcl  14115  rhmmul  14143  rhmdvdsr  14154  subrngmcl  14188  subrgmcl  14212  subrgdv  14217  subrgugrp  14219  domneq0  14251  scafvalg  14286  lmodprop2d  14327  lssclg  14343  lssvnegcl  14355  lssintclm  14363  sralmod  14429  rnglidlmcl  14459  lidlnegcl  14464  rspssp  14473  rnglidlmsgrp  14476  rnglidlrng  14477  2idlcpblrng  14502  qus2idrng  14504  zndvds  14628  znleval2  14633  basgen  14769  2basgeng  14771  iuncld  14804  neipsm  14843  opnneissb  14844  opnssneib  14845  iscnp3  14892  cnprcl2k  14895  cnpnei  14908  cncnp2m  14920  cnptoprest  14928  sslm  14936  upxp  14961  cnmpt22  14983  distspace  15024  0met  15073  blvalps  15077  blval  15078  ssblps  15114  ssbl  15115  blpnfctr  15128  blopn  15179  blnei  15181  bdxmet  15190  bdbl  15192  metcnp3  15200  tgqioo  15244  ptolemy  15513  sinq12gt0  15519  sincosq1eq  15528  rpcxpadd  15594  cxpmul  15601  rplogbval  15634  logbleb  15650  logbgcd1irr  15656  logbprmirr  15661  lgsfvalg  15699  lgsneg1  15719  lgssq  15734  lgsdinn0  15742  gausslemma2dlem1a  15752  2lgs  15798  2lgsoddprmlem2  15800  funvtxdm2domval  15845  funiedgdm2domval  15846  iedgedgg  15876  lpvtx  15894  incistruhgr  15905  ausgrumgrien  15983  ausgrusgrien  15984  umgr2edgneu  16025  ushgredgedg  16039  ushgredgedgloop  16041  iswlk  16064  wlkl1loop  16099  uspgr2wlkeq  16106  istrl  16124  clwwlkccatlem  16137  clwwlkccat  16138  bdfind  16364  1dom1el  16409