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  4440  breldmg  4928  fntpg  5376  funimaexglem  5403  fex2  5491  fvun1  5699  fprg  5821  fsnunfv  5839  fnfvima  5873  cocan1  5910  cocan2  5911  mpoeq3dv  6069  fovcld  6108  fvmpopr2d  6140  funexw  6255  mpofvex  6349  poxp  6376  smoiso  6446  tfrlem5  6458  tfrlemibxssdm  6471  tfr1onlembfn  6488  tfri1dALT  6495  tfrcllembfn  6501  rdgon  6530  freccllem  6546  nnawordex  6673  mapxpen  7005  fidceq  7027  fidifsnen  7028  dif1en  7037  en2eqpr  7065  unsnfi  7077  unsnfidcex  7078  unsnfidcel  7079  fisseneq  7092  ordiso2  7198  updjud  7245  mkvprop  7321  endjudisj  7388  xpdjuen  7396  mulcanenq0ec  7628  prltlu  7670  prarloclem3step  7679  prarloclem5  7683  ltasrg  7953  cnegexlem1  8317  addcan  8322  apcotr  8750  apadd1  8751  mulext1  8755  divdivap1  8866  divdivap2  8867  div2negap  8878  divneg2ap  8879  ltmulgt11  9007  ltdiv2  9030  squeeze0  9047  nndivtr  9148  nn0n0n1ge2  9513  zdivmul  9533  gtndiv  9538  eluzuzle  9726  eluzp1p1  9744  qdivcl  9834  irrmul  9838  rpgecl  9874  xaddass  10061  xltadd1  10068  xlt2add  10072  lbico1  10122  lbicc2  10176  zltaddlt1le  10199  uzsubsubfz  10239  elfz1b  10282  elfz0ubfz0  10317  fz0fzelfz0  10319  difelfzle  10326  difelfznle  10327  2ffzeq  10333  fzo1fzo0n0  10379  ubmelfzo  10401  fzonn0p1p1  10414  elfzom1p1elfzo  10415  elfzonelfzo  10431  subfzo0  10443  ceiqle  10530  ceilqle  10531  modqval  10541  flqpmodeq  10544  modq0  10546  negqmod0  10548  modqge0  10549  modqlt  10550  modqdiffl  10552  modqmulnn  10559  modqvalp1  10560  modqmuladdnn0  10585  qnegmod  10586  addmodid  10589  modfzo0difsn  10612  addmodlteq  10615  qexpclz  10777  expgt1  10794  expp1zap  10805  expm1ap  10806  expubnd  10813  bernneq2  10878  expnlbnd  10881  mulsubdivbinom2ap  10928  omgadd  11019  hashun  11022  fihashssdif  11035  hashdifpr  11037  fimaxq  11044  ccatval2  11128  ccatval3  11129  ccatval1lsw  11134  ccatval21sw  11135  ccatass  11138  ccats1val2  11166  fzowrddc  11174  swrdval  11175  swrdclg  11177  swrdval2  11178  swrdnd  11186  swrdlen2  11189  swrdfv2  11190  ccatswrd  11197  pfxn0  11215  pfxsuff1eqwrdeq  11226  swrdswrdlem  11231  ccats1pfxeq  11241  ccats1pfxeqrex  11242  ccatopth2  11244  wrd2ind  11250  pfxccatin12lem3  11259  pfxccat3  11261  swrdccat  11262  pfxccatpfx2  11264  pfxccat3a  11265  swrdccat3b  11267  pfxccatid  11268  ccats1pfxeqbi  11269  shftuz  11323  mulreap  11370  redivap  11380  imdivap  11387  resqrtcl  11535  xrmaxltsup  11764  xrmaxaddlem  11766  xrmaxadd  11767  xrlemininf  11777  xrminltinf  11778  climuni  11799  addcn2  11816  mulcn2  11818  efsub  12187  sin02gt0  12270  cos12dec  12274  dvdsval2  12296  addmodlteqALT  12365  modremain  12435  fldivndvdslt  12443  mulgcdr  12534  gcddiv  12535  rpmulgcd  12542  rplpwr  12543  rppwr  12544  nnminle  12551  qredeq  12613  divgcdcoprmex  12619  cncongr1  12620  cncongr2  12621  dvdsnprmd  12642  euclemma  12663  prmexpb  12668  qnumdenbi  12709  eulerth  12750  fermltl  12751  prmdiv  12752  hashgcdlem  12755  odzcllem  12760  vfermltl  12769  reumodprminv  12771  modprm0  12772  modprmn0modprm0  12774  coprimeprodsq  12775  pythagtriplem1  12783  pythagtriplem3  12785  pythagtriplem4  12786  pythagtriplem10  12787  pythagtriplem6  12788  pythagtriplem7  12789  pythagtriplem8  12790  pythagtriplem9  12791  pythagtriplem11  12792  pythagtriplem12  12793  pythagtriplem13  12794  pythagtriplem14  12795  pythagtriplem15  12796  pythagtriplem16  12797  pythagtriplem17  12798  pythagtriplem19  12800  pythagtrip  12801  pcpremul  12811  pcdvdsb  12838  dvdsprmpweqnn  12854  dvdsprmpweqle  12855  difsqpwdvds  12856  pcfaclem  12867  pcbc  12869  4sqlem12  12920  unennn  12963  nninfdc  13019  setsex  13059  f1ocpbllem  13338  imasaddfnlemg  13342  imasaddvallemg  13343  ercpbl  13359  erlecpbl  13360  qusaddvallemg  13361  fvprif  13371  xpsfrnel2  13374  plusfvalg  13391  imasmnd  13481  insubm  13513  grpidrcan  13593  grpidlcan  13594  grpsubpropd2  13633  pwsinvg  13640  imasgrp2  13642  imasgrp  13643  mulgnnsubcl  13666  mulgnn0subcl  13667  mulgsubcl  13668  mulgaddcom  13678  mulginvcom  13679  mulgnnass  13689  mulgassr  13692  mulgpropdg  13696  submmulg  13698  subgcl  13716  subgsubcl  13717  subgsub  13718  subgmulg  13720  nsgconj  13738  ghmsub  13783  ghmrn  13789  ghmeqker  13803  f1ghm0to0  13804  ablinvadd  13842  ablsub4  13845  abladdsub4  13846  subcmnd  13865  imasabl  13868  rngcl  13902  imasrng  13914  srgcl  13928  srg1zr  13945  srgen1zr  13946  ringcl  13971  crngcom  13972  ringidss  13987  mulgass2  14016  imasring  14022  opprmulg  14029  unitmulclb  14072  unitdvcl  14094  rhmmul  14122  rhmdvdsr  14133  subrngmcl  14167  subrgmcl  14191  subrgdv  14196  subrgugrp  14198  domneq0  14230  scafvalg  14265  lmodprop2d  14306  lssclg  14322  lssvnegcl  14334  lssintclm  14342  sralmod  14408  rnglidlmcl  14438  lidlnegcl  14443  rspssp  14452  rnglidlmsgrp  14455  rnglidlrng  14456  2idlcpblrng  14481  qus2idrng  14483  zndvds  14607  znleval2  14612  basgen  14748  2basgeng  14750  iuncld  14783  neipsm  14822  opnneissb  14823  opnssneib  14824  iscnp3  14871  cnprcl2k  14874  cnpnei  14887  cncnp2m  14899  cnptoprest  14907  sslm  14915  upxp  14940  cnmpt22  14962  distspace  15003  0met  15052  blvalps  15056  blval  15057  ssblps  15093  ssbl  15094  blpnfctr  15107  blopn  15158  blnei  15160  bdxmet  15169  bdbl  15171  metcnp3  15179  tgqioo  15223  ptolemy  15492  sinq12gt0  15498  sincosq1eq  15507  rpcxpadd  15573  cxpmul  15580  rplogbval  15613  logbleb  15629  logbgcd1irr  15635  logbprmirr  15640  lgsfvalg  15678  lgsneg1  15698  lgssq  15713  lgsdinn0  15721  gausslemma2dlem1a  15731  2lgs  15777  2lgsoddprmlem2  15779  funvtxdm2domval  15824  funiedgdm2domval  15825  iedgedgg  15855  lpvtx  15873  incistruhgr  15884  ausgrumgrien  15962  ausgrusgrien  15963  umgr2edgneu  16004  ushgredgedg  16018  ushgredgedgloop  16020  iswlk  16029  bdfind  16267  1dom1el  16312