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  2764  sbciegft  2994  reupick2  3422  ifbothdc  3568  frirrg  4351  breldmg  4834  fntpg  5273  funimaexglem  5300  fex2  5385  fvun1  5583  fprg  5700  fsnunfv  5718  fnfvima  5752  cocan1  5788  cocan2  5789  mpoeq3dv  5941  funexw  6113  mpofvex  6204  poxp  6233  smoiso  6303  tfrlem5  6315  tfrlemibxssdm  6328  tfr1onlembfn  6345  tfri1dALT  6352  tfrcllembfn  6358  rdgon  6387  freccllem  6403  nnawordex  6530  mapxpen  6848  fidceq  6869  fidifsnen  6870  dif1en  6879  en2eqpr  6907  unsnfi  6918  unsnfidcex  6919  unsnfidcel  6920  fisseneq  6931  ordiso2  7034  updjud  7081  mkvprop  7156  endjudisj  7209  xpdjuen  7217  mulcanenq0ec  7444  prltlu  7486  prarloclem3step  7495  prarloclem5  7499  ltasrg  7769  cnegexlem1  8132  addcan  8137  apcotr  8564  apadd1  8565  mulext1  8569  divdivap1  8680  divdivap2  8681  div2negap  8692  divneg2ap  8693  ltmulgt11  8821  ltdiv2  8844  squeeze0  8861  nndivtr  8961  nn0n0n1ge2  9323  zdivmul  9343  gtndiv  9348  eluzuzle  9536  eluzp1p1  9553  qdivcl  9643  irrmul  9647  rpgecl  9682  xaddass  9869  xltadd1  9876  xlt2add  9880  lbico1  9930  lbicc2  9984  zltaddlt1le  10007  uzsubsubfz  10047  elfz1b  10090  elfz0ubfz0  10125  fz0fzelfz0  10127  difelfzle  10134  difelfznle  10135  2ffzeq  10141  fzo1fzo0n0  10183  ubmelfzo  10200  fzonn0p1p1  10213  elfzom1p1elfzo  10214  elfzonelfzo  10230  subfzo0  10242  ceiqle  10313  ceilqle  10314  modqval  10324  flqpmodeq  10327  modq0  10329  negqmod0  10331  modqge0  10332  modqlt  10333  modqdiffl  10335  modqmulnn  10342  modqvalp1  10343  modqmuladdnn0  10368  qnegmod  10369  addmodid  10372  modfzo0difsn  10395  addmodlteq  10398  qexpclz  10541  expgt1  10558  expp1zap  10569  expm1ap  10570  expubnd  10577  bernneq2  10642  expnlbnd  10645  mulsubdivbinom2ap  10691  omgadd  10782  hashun  10785  fihashssdif  10798  hashdifpr  10800  fimaxq  10807  shftuz  10826  mulreap  10873  redivap  10883  imdivap  10890  resqrtcl  11038  xrmaxltsup  11266  xrmaxaddlem  11268  xrmaxadd  11269  xrlemininf  11279  xrminltinf  11280  climuni  11301  addcn2  11318  mulcn2  11320  efsub  11689  sin02gt0  11771  cos12dec  11775  dvdsval2  11797  addmodlteqALT  11865  modremain  11934  fldivndvdslt  11940  mulgcdr  12019  gcddiv  12020  rpmulgcd  12027  rplpwr  12028  rppwr  12029  nnminle  12036  qredeq  12096  divgcdcoprmex  12102  cncongr1  12103  cncongr2  12104  dvdsnprmd  12125  euclemma  12146  prmexpb  12151  qnumdenbi  12192  eulerth  12233  fermltl  12234  prmdiv  12235  hashgcdlem  12238  odzcllem  12242  vfermltl  12251  reumodprminv  12253  modprm0  12254  modprmn0modprm0  12256  coprimeprodsq  12257  pythagtriplem1  12265  pythagtriplem3  12267  pythagtriplem4  12268  pythagtriplem10  12269  pythagtriplem6  12270  pythagtriplem7  12271  pythagtriplem8  12272  pythagtriplem9  12273  pythagtriplem11  12274  pythagtriplem12  12275  pythagtriplem13  12276  pythagtriplem14  12277  pythagtriplem15  12278  pythagtriplem16  12279  pythagtriplem17  12280  pythagtriplem19  12282  pythagtrip  12283  pcpremul  12293  pcdvdsb  12319  dvdsprmpweqnn  12335  dvdsprmpweqle  12336  difsqpwdvds  12337  pcfaclem  12347  pcbc  12349  unennn  12398  nninfdc  12454  setsex  12494  f1ocpbllem  12731  imasaddfnlemg  12735  imasaddvallemg  12736  ercpbl  12750  erlecpbl  12751  qusaddvallemg  12752  fvprif  12762  xpsfrnel2  12765  plusfvalg  12782  insubm  12872  grpidrcan  12935  grpidlcan  12936  grpsubpropd2  12975  mulgnnsubcl  12995  mulgnn0subcl  12996  mulgsubcl  12997  mulgaddcom  13007  mulginvcom  13008  mulgnnass  13018  mulgassr  13021  mulgpropdg  13025  subgcl  13044  subgsubcl  13045  subgsub  13046  subgmulg  13048  nsgconj  13066  ablinvadd  13113  ablsub4  13116  abladdsub4  13117  subcmnd  13129  srgcl  13153  srg1zr  13170  srgen1zr  13171  ringcl  13196  crngcom  13197  ringidss  13212  mulgass2  13235  opprmulg  13243  unitmulclb  13283  unitdvcl  13305  subrgmcl  13354  subrgdv  13359  subrgugrp  13361  scafvalg  13397  lmodprop2d  13438  basgen  13583  2basgeng  13585  iuncld  13618  neipsm  13657  opnneissb  13658  opnssneib  13659  iscnp3  13706  cnprcl2k  13709  cnpnei  13722  cncnp2m  13734  cnptoprest  13742  sslm  13750  upxp  13775  cnmpt22  13797  distspace  13838  0met  13887  blvalps  13891  blval  13892  ssblps  13928  ssbl  13929  blpnfctr  13942  blopn  13993  blnei  13995  bdxmet  14004  bdbl  14006  metcnp3  14014  tgqioo  14050  ptolemy  14248  sinq12gt0  14254  sincosq1eq  14263  rpcxpadd  14329  cxpmul  14336  rplogbval  14366  logbleb  14382  logbgcd1irr  14388  logbprmirr  14393  lgsfvalg  14409  lgsneg1  14429  lgssq  14444  lgsdinn0  14452  2lgsoddprmlem2  14457  bdfind  14701