Theorem 3ad2ant1 1045

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  simp1l  1048  simp1r  1049  simp11  1054  simp12  1055  simp13  1056  simp1ll  1087  simp1lr  1088  simp1rl  1089  simp1rr  1090  simp1l1  1117  simp1l2  1118  simp1l3  1119  simp1r1  1120  simp1r2  1121  simp1r3  1122  simp11l  1135  simp11r  1136  simp12l  1137  simp12r  1138  simp13l  1139  simp13r  1140  simp111  1153  simp112  1154  simp113  1155  simp121  1156  simp122  1157  simp123  1158  simp131  1159  simp132  1160  simp133  1161  3anim123i  1211  3jaao  1345  ceqsalt  2840  sbciegft  3073  reupick2  3507  ifbothdc  3657  frirrg  4471  breldmg  4962  fntpg  5412  funimaexglem  5439  fex2  5531  fresaunres2disj  5545  fvun1  5743  fprg  5867  fsnunfv  5885  fnfvima  5921  cocan1  5960  cocan2  5961  mpoeq3dv  6119  fovcld  6158  fvmpopr2d  6190  funexw  6305  mpofvex  6401  poxp  6428  suppval1  6439  suppvalfng  6440  suppvalfn  6441  suppimacnvfn  6446  suppsnopdc  6450  smoiso  6533  tfrlem5  6545  tfrlemibxssdm  6558  tfr1onlembfn  6575  tfri1dALT  6582  tfrcllembfn  6588  rdgon  6617  freccllem  6633  nnawordex  6762  1dom1el  7060  mapxpen  7101  fidceq  7124  fidifsnen  7125  dif1en  7136  en2eqpr  7167  unsnfi  7179  unsnfidcex  7180  unsnfidcel  7181  fisseneq  7195  funisfsupp  7244  ordiso2  7326  updjud  7373  mkvprop  7449  endjudisj  7517  xpdjuen  7525  mulcanenq0ec  7760  prltlu  7802  prarloclem3step  7811  prarloclem5  7815  ltasrg  8085  cnegexlem1  8448  addcan  8453  apcotr  8881  apadd1  8882  mulext1  8886  divdivap1  8997  divdivap2  8998  div2negap  9009  divneg2ap  9010  ltmulgt11  9138  ltdiv2  9161  squeeze0  9178  nndivtr  9279  nn0n0n1ge2  9648  zdivmul  9668  gtndiv  9673  eluzuzle  9862  eluzp1p1  9880  qdivcl  9975  irrmul  9979  rpgecl  10015  xaddass  10202  xltadd1  10209  xlt2add  10213  lbico1  10263  lbicc2  10317  zltaddlt1le  10341  uzsubsubfz  10381  elfz1b  10424  elfz0ubfz0  10459  fz0fzelfz0  10461  difelfzle  10468  difelfznle  10469  2ffzeq  10475  fzo1fzo0n0  10522  ubmelfzo  10545  fzonn0p1p1  10558  elfzom1p1elfzo  10559  elfzonelfzo  10575  subfzo0  10588  ceiqle  10675  ceilqle  10676  modqval  10686  flqpmodeq  10689  modq0  10691  negqmod0  10693  modqge0  10694  modqlt  10695  modqdiffl  10697  modqmulnn  10704  modqvalp1  10705  modqmuladdnn0  10730  qnegmod  10731  addmodid  10734  modfzo0difsn  10757  addmodlteq  10760  qexpclz  10922  expgt1  10939  expp1zap  10950  expm1ap  10951  expubnd  10958  bernneq2  11023  expnlbnd  11026  mulsubdivbinom2ap  11073  omgadd  11166  hashun  11169  fihashssdif  11183  hashdifpr  11185  fimaxq  11194  ccatval2  11286  ccatval3  11287  ccatval1lsw  11292  ccatval21sw  11293  ccatass  11296  ccatw2s1leng  11326  ccats1val2  11328  ccat2s1fvwd  11335  fzowrddc  11339  swrdval  11340  swrdclg  11342  swrdval2  11343  swrdnd  11351  swrdlen2  11354  swrdfv2  11355  ccatswrd  11362  pfxn0  11380  pfxsuff1eqwrdeq  11391  swrdswrdlem  11396  ccats1pfxeq  11406  ccats1pfxeqrex  11407  ccatopth2  11409  wrd2ind  11415  pfxccatin12lem3  11424  pfxccat3  11426  swrdccat  11427  pfxccatpfx2  11429  pfxccat3a  11430  swrdccat3b  11432  pfxccatid  11433  ccats1pfxeqbi  11434  shftuz  11502  mulreap  11549  redivap  11559  imdivap  11566  resqrtcl  11714  xrmaxltsup  11943  xrmaxaddlem  11945  xrmaxadd  11946  xrlemininf  11956  xrminltinf  11957  climuni  11978  addcn2  11995  mulcn2  11997  efsub  12367  sin02gt0  12450  cos12dec  12454  dvdsval2  12476  addmodlteqALT  12545  modremain  12615  fldivndvdslt  12623  mulgcdr  12714  gcddiv  12715  rpmulgcd  12722  rplpwr  12723  rppwr  12724  nnminle  12731  qredeq  12793  divgcdcoprmex  12799  cncongr1  12800  cncongr2  12801  dvdsnprmd  12822  euclemma  12843  prmexpb  12848  qnumdenbi  12889  eulerth  12930  fermltl  12931  prmdiv  12932  hashgcdlem  12935  odzcllem  12940  vfermltl  12949  reumodprminv  12951  modprm0  12952  modprmn0modprm0  12954  coprimeprodsq  12955  pythagtriplem1  12963  pythagtriplem3  12965  pythagtriplem4  12966  pythagtriplem10  12967  pythagtriplem6  12968  pythagtriplem7  12969  pythagtriplem8  12970  pythagtriplem9  12971  pythagtriplem11  12972  pythagtriplem12  12973  pythagtriplem13  12974  pythagtriplem14  12975  pythagtriplem15  12976  pythagtriplem16  12977  pythagtriplem17  12978  pythagtriplem19  12980  pythagtrip  12981  pcpremul  12991  pcdvdsb  13018  dvdsprmpweqnn  13034  dvdsprmpweqle  13035  difsqpwdvds  13036  pcfaclem  13047  pcbc  13049  4sqlem12  13100  unennn  13148  nninfdc  13204  setsex  13244  f1ocpbllem  13523  imasaddfnlemg  13527  imasaddvallemg  13528  ercpbl  13544  erlecpbl  13545  qusaddvallemg  13546  fvprif  13556  xpsfrnel2  13559  plusfvalg  13576  imasmnd  13666  insubm  13698  grpidrcan  13778  grpidlcan  13779  grpsubpropd2  13818  pwsinvg  13825  imasgrp2  13827  imasgrp  13828  mulgnnsubcl  13851  mulgnn0subcl  13852  mulgsubcl  13853  mulgaddcom  13863  mulginvcom  13864  mulgnnass  13874  mulgassr  13877  mulgpropdg  13881  submmulg  13883  subgcl  13901  subgsubcl  13902  subgsub  13903  subgmulg  13905  nsgconj  13923  ghmsub  13968  ghmrn  13974  ghmeqker  13988  f1ghm0to0  13989  ablinvadd  14027  ablsub4  14030  abladdsub4  14031  subcmnd  14050  imasabl  14053  rngcl  14088  imasrng  14100  srgcl  14114  srg1zr  14131  srgen1zr  14132  ringcl  14157  crngcom  14158  ringidss  14173  mulgass2  14202  imasring  14208  opprmulg  14215  unitmulclb  14259  unitdvcl  14281  rhmmul  14309  rhmdvdsr  14320  subrngmcl  14354  subrgmcl  14378  subrgdv  14383  subrgugrp  14385  domneq0  14418  scafvalg  14455  lmodprop2d  14496  lssclg  14512  lssvnegcl  14524  lssintclm  14532  sralmod  14598  rnglidlmcl  14628  lidlnegcl  14633  rspssp  14642  rnglidlmsgrp  14645  rnglidlrng  14646  2idlcpblrng  14671  qus2idrng  14673  zndvds  14797  znleval2  14802  psrbaglesupp  14822  psrbaglecl  14824  psrbagaddclfi  14825  psrbagcon  14826  basgen  14945  2basgeng  14947  iuncld  14980  neipsm  15019  opnneissb  15020  opnssneib  15021  iscnp3  15068  cnprcl2k  15071  cnpnei  15084  cncnp2m  15096  cnptoprest  15104  sslm  15112  upxp  15137  cnmpt22  15159  distspace  15200  0met  15249  blvalps  15253  blval  15254  ssblps  15290  ssbl  15291  blpnfctr  15304  blopn  15355  blnei  15357  bdxmet  15366  bdbl  15368  metcnp3  15376  tgqioo  15420  ptolemy  15689  sinq12gt0  15695  sincosq1eq  15704  rpcxpadd  15770  cxpmul  15777  rplogbval  15810  logbleb  15826  logbgcd1irr  15832  logbprmirr  15837  pellexlem1  15845  lgsfvalg  15878  lgsneg1  15898  lgssq  15913  lgsdinn0  15921  gausslemma2dlem1a  15931  2lgs  15977  2lgsoddprmlem2  15979  funvtxdm2domval  16024  funiedgdm2domval  16025  iedgedgg  16056  lpvtx  16074  incistruhgr  16085  ausgrumgrien  16165  ausgrusgrien  16166  umgr2edgneu  16207  ushgredgedg  16221  ushgredgedgloop  16223  usgr2v1e2w  16241  egrsubgr  16258  subumgredg2en  16266  iswlk  16318  wlkl1loop  16353  uspgr2wlkeq  16360  istrl  16380  clwwlkccatlem  16395  clwwlkccat  16396  clwwlknccat  16418  clwwlknonex2lem2  16433  clwwlknonex2  16434  iseupth  16442  eupth2lem3lem6fi  16466  konigsbergssiedgwen  16481  bdfind  16716  repiecele0  16810  repiecege0  16811