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  2827  sbciegft  3060  reupick2  3491  ifbothdc  3638  frirrg  4445  breldmg  4935  fntpg  5383  funimaexglem  5410  fex2  5500  fvun1  5708  fprg  5832  fsnunfv  5850  fnfvima  5884  cocan1  5923  cocan2  5924  mpoeq3dv  6082  fovcld  6121  fvmpopr2d  6153  funexw  6269  mpofvex  6365  poxp  6392  smoiso  6463  tfrlem5  6475  tfrlemibxssdm  6488  tfr1onlembfn  6505  tfri1dALT  6512  tfrcllembfn  6518  rdgon  6547  freccllem  6563  nnawordex  6692  1dom1el  6988  mapxpen  7029  fidceq  7051  fidifsnen  7052  dif1en  7061  en2eqpr  7092  unsnfi  7104  unsnfidcex  7105  unsnfidcel  7106  fisseneq  7119  ordiso2  7225  updjud  7272  mkvprop  7348  endjudisj  7415  xpdjuen  7423  mulcanenq0ec  7655  prltlu  7697  prarloclem3step  7706  prarloclem5  7710  ltasrg  7980  cnegexlem1  8344  addcan  8349  apcotr  8777  apadd1  8778  mulext1  8782  divdivap1  8893  divdivap2  8894  div2negap  8905  divneg2ap  8906  ltmulgt11  9034  ltdiv2  9057  squeeze0  9074  nndivtr  9175  nn0n0n1ge2  9540  zdivmul  9560  gtndiv  9565  eluzuzle  9754  eluzp1p1  9772  qdivcl  9867  irrmul  9871  rpgecl  9907  xaddass  10094  xltadd1  10101  xlt2add  10105  lbico1  10155  lbicc2  10209  zltaddlt1le  10232  uzsubsubfz  10272  elfz1b  10315  elfz0ubfz0  10350  fz0fzelfz0  10352  difelfzle  10359  difelfznle  10360  2ffzeq  10366  fzo1fzo0n0  10412  ubmelfzo  10435  fzonn0p1p1  10448  elfzom1p1elfzo  10449  elfzonelfzo  10465  subfzo0  10478  ceiqle  10565  ceilqle  10566  modqval  10576  flqpmodeq  10579  modq0  10581  negqmod0  10583  modqge0  10584  modqlt  10585  modqdiffl  10587  modqmulnn  10594  modqvalp1  10595  modqmuladdnn0  10620  qnegmod  10621  addmodid  10624  modfzo0difsn  10647  addmodlteq  10650  qexpclz  10812  expgt1  10829  expp1zap  10840  expm1ap  10841  expubnd  10848  bernneq2  10913  expnlbnd  10916  mulsubdivbinom2ap  10963  omgadd  11055  hashun  11058  fihashssdif  11072  hashdifpr  11074  fimaxq  11081  ccatval2  11165  ccatval3  11166  ccatval1lsw  11171  ccatval21sw  11172  ccatass  11175  ccatw2s1leng  11205  ccats1val2  11207  ccat2s1fvwd  11214  fzowrddc  11218  swrdval  11219  swrdclg  11221  swrdval2  11222  swrdnd  11230  swrdlen2  11233  swrdfv2  11234  ccatswrd  11241  pfxn0  11259  pfxsuff1eqwrdeq  11270  swrdswrdlem  11275  ccats1pfxeq  11285  ccats1pfxeqrex  11286  ccatopth2  11288  wrd2ind  11294  pfxccatin12lem3  11303  pfxccat3  11305  swrdccat  11306  pfxccatpfx2  11308  pfxccat3a  11309  swrdccat3b  11311  pfxccatid  11312  ccats1pfxeqbi  11313  shftuz  11368  mulreap  11415  redivap  11425  imdivap  11432  resqrtcl  11580  xrmaxltsup  11809  xrmaxaddlem  11811  xrmaxadd  11812  xrlemininf  11822  xrminltinf  11823  climuni  11844  addcn2  11861  mulcn2  11863  efsub  12232  sin02gt0  12315  cos12dec  12319  dvdsval2  12341  addmodlteqALT  12410  modremain  12480  fldivndvdslt  12488  mulgcdr  12579  gcddiv  12580  rpmulgcd  12587  rplpwr  12588  rppwr  12589  nnminle  12596  qredeq  12658  divgcdcoprmex  12664  cncongr1  12665  cncongr2  12666  dvdsnprmd  12687  euclemma  12708  prmexpb  12713  qnumdenbi  12754  eulerth  12795  fermltl  12796  prmdiv  12797  hashgcdlem  12800  odzcllem  12805  vfermltl  12814  reumodprminv  12816  modprm0  12817  modprmn0modprm0  12819  coprimeprodsq  12820  pythagtriplem1  12828  pythagtriplem3  12830  pythagtriplem4  12831  pythagtriplem10  12832  pythagtriplem6  12833  pythagtriplem7  12834  pythagtriplem8  12835  pythagtriplem9  12836  pythagtriplem11  12837  pythagtriplem12  12838  pythagtriplem13  12839  pythagtriplem14  12840  pythagtriplem15  12841  pythagtriplem16  12842  pythagtriplem17  12843  pythagtriplem19  12845  pythagtrip  12846  pcpremul  12856  pcdvdsb  12883  dvdsprmpweqnn  12899  dvdsprmpweqle  12900  difsqpwdvds  12901  pcfaclem  12912  pcbc  12914  4sqlem12  12965  unennn  13008  nninfdc  13064  setsex  13104  f1ocpbllem  13383  imasaddfnlemg  13387  imasaddvallemg  13388  ercpbl  13404  erlecpbl  13405  qusaddvallemg  13406  fvprif  13416  xpsfrnel2  13419  plusfvalg  13436  imasmnd  13526  insubm  13558  grpidrcan  13638  grpidlcan  13639  grpsubpropd2  13678  pwsinvg  13685  imasgrp2  13687  imasgrp  13688  mulgnnsubcl  13711  mulgnn0subcl  13712  mulgsubcl  13713  mulgaddcom  13723  mulginvcom  13724  mulgnnass  13734  mulgassr  13737  mulgpropdg  13741  submmulg  13743  subgcl  13761  subgsubcl  13762  subgsub  13763  subgmulg  13765  nsgconj  13783  ghmsub  13828  ghmrn  13834  ghmeqker  13848  f1ghm0to0  13849  ablinvadd  13887  ablsub4  13890  abladdsub4  13891  subcmnd  13910  imasabl  13913  rngcl  13947  imasrng  13959  srgcl  13973  srg1zr  13990  srgen1zr  13991  ringcl  14016  crngcom  14017  ringidss  14032  mulgass2  14061  imasring  14067  opprmulg  14074  unitmulclb  14118  unitdvcl  14140  rhmmul  14168  rhmdvdsr  14179  subrngmcl  14213  subrgmcl  14237  subrgdv  14242  subrgugrp  14244  domneq0  14276  scafvalg  14311  lmodprop2d  14352  lssclg  14368  lssvnegcl  14380  lssintclm  14388  sralmod  14454  rnglidlmcl  14484  lidlnegcl  14489  rspssp  14498  rnglidlmsgrp  14501  rnglidlrng  14502  2idlcpblrng  14527  qus2idrng  14529  zndvds  14653  znleval2  14658  basgen  14794  2basgeng  14796  iuncld  14829  neipsm  14868  opnneissb  14869  opnssneib  14870  iscnp3  14917  cnprcl2k  14920  cnpnei  14933  cncnp2m  14945  cnptoprest  14953  sslm  14961  upxp  14986  cnmpt22  15008  distspace  15049  0met  15098  blvalps  15102  blval  15103  ssblps  15139  ssbl  15140  blpnfctr  15153  blopn  15204  blnei  15206  bdxmet  15215  bdbl  15217  metcnp3  15225  tgqioo  15269  ptolemy  15538  sinq12gt0  15544  sincosq1eq  15553  rpcxpadd  15619  cxpmul  15626  rplogbval  15659  logbleb  15675  logbgcd1irr  15681  logbprmirr  15686  lgsfvalg  15724  lgsneg1  15744  lgssq  15759  lgsdinn0  15767  gausslemma2dlem1a  15777  2lgs  15823  2lgsoddprmlem2  15825  funvtxdm2domval  15870  funiedgdm2domval  15871  iedgedgg  15902  lpvtx  15920  incistruhgr  15931  ausgrumgrien  16009  ausgrusgrien  16010  umgr2edgneu  16051  ushgredgedg  16065  ushgredgedgloop  16067  usgr2v1e2w  16085  iswlk  16120  wlkl1loop  16155  uspgr2wlkeq  16162  istrl  16180  clwwlkccatlem  16195  clwwlkccat  16196  clwwlknccat  16218  clwwlknonex2lem2  16233  clwwlknonex2  16234  iseupth  16242  bdfind  16477