Theorem 3ad2ant1 1018

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

Syntax hints:   → wi 4   ∧ w3a 978

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 980

This theorem is referenced by:  simp1l  1021  simp1r  1022  simp11  1027  simp12  1028  simp13  1029  simp1ll  1060  simp1lr  1061  simp1rl  1062  simp1rr  1063  simp1l1  1090  simp1l2  1091  simp1l3  1092  simp1r1  1093  simp1r2  1094  simp1r3  1095  simp11l  1108  simp11r  1109  simp12l  1110  simp12r  1111  simp13l  1112  simp13r  1113  simp111  1126  simp112  1127  simp113  1128  simp121  1129  simp122  1130  simp123  1131  simp131  1132  simp132  1133  simp133  1134  3anim123i  1184  3jaao  1308  ceqsalt  2763  sbciegft  2993  reupick2  3421  ifbothdc  3567  frirrg  4350  breldmg  4833  fntpg  5272  funimaexglem  5299  fex2  5384  fvun1  5582  fprg  5699  fsnunfv  5717  fnfvima  5751  cocan1  5787  cocan2  5788  mpoeq3dv  5940  funexw  6112  mpofvex  6203  poxp  6232  smoiso  6302  tfrlem5  6314  tfrlemibxssdm  6327  tfr1onlembfn  6344  tfri1dALT  6351  tfrcllembfn  6357  rdgon  6386  freccllem  6402  nnawordex  6529  mapxpen  6847  fidceq  6868  fidifsnen  6869  dif1en  6878  en2eqpr  6906  unsnfi  6917  unsnfidcex  6918  unsnfidcel  6919  fisseneq  6930  ordiso2  7033  updjud  7080  mkvprop  7155  endjudisj  7208  xpdjuen  7216  mulcanenq0ec  7443  prltlu  7485  prarloclem3step  7494  prarloclem5  7498  ltasrg  7768  cnegexlem1  8131  addcan  8136  apcotr  8563  apadd1  8564  mulext1  8568  divdivap1  8679  divdivap2  8680  div2negap  8691  divneg2ap  8692  ltmulgt11  8820  ltdiv2  8843  squeeze0  8860  nndivtr  8960  nn0n0n1ge2  9322  zdivmul  9342  gtndiv  9347  eluzuzle  9535  eluzp1p1  9552  qdivcl  9642  irrmul  9646  rpgecl  9681  xaddass  9868  xltadd1  9875  xlt2add  9879  lbico1  9929  lbicc2  9983  zltaddlt1le  10006  uzsubsubfz  10046  elfz1b  10089  elfz0ubfz0  10124  fz0fzelfz0  10126  difelfzle  10133  difelfznle  10134  2ffzeq  10140  fzo1fzo0n0  10182  ubmelfzo  10199  fzonn0p1p1  10212  elfzom1p1elfzo  10213  elfzonelfzo  10229  subfzo0  10241  ceiqle  10312  ceilqle  10313  modqval  10323  flqpmodeq  10326  modq0  10328  negqmod0  10330  modqge0  10331  modqlt  10332  modqdiffl  10334  modqmulnn  10341  modqvalp1  10342  modqmuladdnn0  10367  qnegmod  10368  addmodid  10371  modfzo0difsn  10394  addmodlteq  10397  qexpclz  10540  expgt1  10557  expp1zap  10568  expm1ap  10569  expubnd  10576  bernneq2  10641  expnlbnd  10644  mulsubdivbinom2ap  10690  omgadd  10781  hashun  10784  fihashssdif  10797  hashdifpr  10799  fimaxq  10806  shftuz  10825  mulreap  10872  redivap  10882  imdivap  10889  resqrtcl  11037  xrmaxltsup  11265  xrmaxaddlem  11267  xrmaxadd  11268  xrlemininf  11278  xrminltinf  11279  climuni  11300  addcn2  11317  mulcn2  11319  efsub  11688  sin02gt0  11770  cos12dec  11774  dvdsval2  11796  addmodlteqALT  11864  modremain  11933  fldivndvdslt  11939  mulgcdr  12018  gcddiv  12019  rpmulgcd  12026  rplpwr  12027  rppwr  12028  nnminle  12035  qredeq  12095  divgcdcoprmex  12101  cncongr1  12102  cncongr2  12103  dvdsnprmd  12124  euclemma  12145  prmexpb  12150  qnumdenbi  12191  eulerth  12232  fermltl  12233  prmdiv  12234  hashgcdlem  12237  odzcllem  12241  vfermltl  12250  reumodprminv  12252  modprm0  12253  modprmn0modprm0  12255  coprimeprodsq  12256  pythagtriplem1  12264  pythagtriplem3  12266  pythagtriplem4  12267  pythagtriplem10  12268  pythagtriplem6  12269  pythagtriplem7  12270  pythagtriplem8  12271  pythagtriplem9  12272  pythagtriplem11  12273  pythagtriplem12  12274  pythagtriplem13  12275  pythagtriplem14  12276  pythagtriplem15  12277  pythagtriplem16  12278  pythagtriplem17  12279  pythagtriplem19  12281  pythagtrip  12282  pcpremul  12292  pcdvdsb  12318  dvdsprmpweqnn  12334  dvdsprmpweqle  12335  difsqpwdvds  12336  pcfaclem  12346  pcbc  12348  unennn  12397  nninfdc  12453  setsex  12493  f1ocpbllem  12730  imasaddfnlemg  12734  imasaddvallemg  12735  ercpbl  12749  erlecpbl  12750  qusaddvallemg  12751  fvprif  12761  xpsfrnel2  12764  plusfvalg  12781  insubm  12871  grpidrcan  12934  grpidlcan  12935  grpsubpropd2  12974  mulgnnsubcl  12994  mulgnn0subcl  12995  mulgsubcl  12996  mulgaddcom  13005  mulginvcom  13006  mulgnnass  13016  mulgassr  13019  mulgpropdg  13023  subgcl  13042  subgsubcl  13043  subgsub  13044  subgmulg  13046  nsgconj  13064  ablinvadd  13111  ablsub4  13114  abladdsub4  13115  subcmnd  13127  srgcl  13151  srg1zr  13168  srgen1zr  13169  ringcl  13194  crngcom  13195  ringidss  13210  mulgass2  13233  opprmulg  13241  unitmulclb  13281  unitdvcl  13303  subrgmcl  13352  subrgdv  13357  subrgugrp  13359  scafvalg  13395  basgen  13550  2basgeng  13552  iuncld  13585  neipsm  13624  opnneissb  13625  opnssneib  13626  iscnp3  13673  cnprcl2k  13676  cnpnei  13689  cncnp2m  13701  cnptoprest  13709  sslm  13717  upxp  13742  cnmpt22  13764  distspace  13805  0met  13854  blvalps  13858  blval  13859  ssblps  13895  ssbl  13896  blpnfctr  13909  blopn  13960  blnei  13962  bdxmet  13971  bdbl  13973  metcnp3  13981  tgqioo  14017  ptolemy  14215  sinq12gt0  14221  sincosq1eq  14230  rpcxpadd  14296  cxpmul  14303  rplogbval  14333  logbleb  14349  logbgcd1irr  14355  logbprmirr  14360  lgsfvalg  14376  lgsneg1  14396  lgssq  14411  lgsdinn0  14419  2lgsoddprmlem2  14424  bdfind  14668