Theorem 3ad2ant1 1021

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

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  simp1l  1024  simp1r  1025  simp11  1030  simp12  1031  simp13  1032  simp1ll  1063  simp1lr  1064  simp1rl  1065  simp1rr  1066  simp1l1  1093  simp1l2  1094  simp1l3  1095  simp1r1  1096  simp1r2  1097  simp1r3  1098  simp11l  1111  simp11r  1112  simp12l  1113  simp12r  1114  simp13l  1115  simp13r  1116  simp111  1129  simp112  1130  simp113  1131  simp121  1132  simp122  1133  simp123  1134  simp131  1135  simp132  1136  simp133  1137  3anim123i  1187  3jaao  1321  ceqsalt  2798  sbciegft  3029  reupick2  3459  ifbothdc  3605  frirrg  4397  breldmg  4884  fntpg  5330  funimaexglem  5357  fex2  5444  fvun1  5645  fprg  5767  fsnunfv  5785  fnfvima  5819  cocan1  5856  cocan2  5857  mpoeq3dv  6011  fovcld  6050  fvmpopr2d  6082  funexw  6197  mpofvex  6291  poxp  6318  smoiso  6388  tfrlem5  6400  tfrlemibxssdm  6413  tfr1onlembfn  6430  tfri1dALT  6437  tfrcllembfn  6443  rdgon  6472  freccllem  6488  nnawordex  6615  mapxpen  6945  fidceq  6966  fidifsnen  6967  dif1en  6976  en2eqpr  7004  unsnfi  7016  unsnfidcex  7017  unsnfidcel  7018  fisseneq  7031  ordiso2  7137  updjud  7184  mkvprop  7260  endjudisj  7322  xpdjuen  7330  mulcanenq0ec  7558  prltlu  7600  prarloclem3step  7609  prarloclem5  7613  ltasrg  7883  cnegexlem1  8247  addcan  8252  apcotr  8680  apadd1  8681  mulext1  8685  divdivap1  8796  divdivap2  8797  div2negap  8808  divneg2ap  8809  ltmulgt11  8937  ltdiv2  8960  squeeze0  8977  nndivtr  9078  nn0n0n1ge2  9443  zdivmul  9463  gtndiv  9468  eluzuzle  9656  eluzp1p1  9674  qdivcl  9764  irrmul  9768  rpgecl  9804  xaddass  9991  xltadd1  9998  xlt2add  10002  lbico1  10052  lbicc2  10106  zltaddlt1le  10129  uzsubsubfz  10169  elfz1b  10212  elfz0ubfz0  10247  fz0fzelfz0  10249  difelfzle  10256  difelfznle  10257  2ffzeq  10263  fzo1fzo0n0  10307  ubmelfzo  10329  fzonn0p1p1  10342  elfzom1p1elfzo  10343  elfzonelfzo  10359  subfzo0  10371  ceiqle  10458  ceilqle  10459  modqval  10469  flqpmodeq  10472  modq0  10474  negqmod0  10476  modqge0  10477  modqlt  10478  modqdiffl  10480  modqmulnn  10487  modqvalp1  10488  modqmuladdnn0  10513  qnegmod  10514  addmodid  10517  modfzo0difsn  10540  addmodlteq  10543  qexpclz  10705  expgt1  10722  expp1zap  10733  expm1ap  10734  expubnd  10741  bernneq2  10806  expnlbnd  10809  mulsubdivbinom2ap  10856  omgadd  10947  hashun  10950  fihashssdif  10963  hashdifpr  10965  fimaxq  10972  ccatval2  11054  ccatval3  11055  ccatval1lsw  11060  ccatval21sw  11061  ccatass  11064  ccats1val2  11092  fzowrddc  11100  swrdval  11101  swrdclg  11103  swrdval2  11104  swrdnd  11112  swrdlen2  11115  swrdfv2  11116  ccatswrd  11123  shftuz  11128  mulreap  11175  redivap  11185  imdivap  11192  resqrtcl  11340  xrmaxltsup  11569  xrmaxaddlem  11571  xrmaxadd  11572  xrlemininf  11582  xrminltinf  11583  climuni  11604  addcn2  11621  mulcn2  11623  efsub  11992  sin02gt0  12075  cos12dec  12079  dvdsval2  12101  addmodlteqALT  12170  modremain  12240  fldivndvdslt  12248  mulgcdr  12339  gcddiv  12340  rpmulgcd  12347  rplpwr  12348  rppwr  12349  nnminle  12356  qredeq  12418  divgcdcoprmex  12424  cncongr1  12425  cncongr2  12426  dvdsnprmd  12447  euclemma  12468  prmexpb  12473  qnumdenbi  12514  eulerth  12555  fermltl  12556  prmdiv  12557  hashgcdlem  12560  odzcllem  12565  vfermltl  12574  reumodprminv  12576  modprm0  12577  modprmn0modprm0  12579  coprimeprodsq  12580  pythagtriplem1  12588  pythagtriplem3  12590  pythagtriplem4  12591  pythagtriplem10  12592  pythagtriplem6  12593  pythagtriplem7  12594  pythagtriplem8  12595  pythagtriplem9  12596  pythagtriplem11  12597  pythagtriplem12  12598  pythagtriplem13  12599  pythagtriplem14  12600  pythagtriplem15  12601  pythagtriplem16  12602  pythagtriplem17  12603  pythagtriplem19  12605  pythagtrip  12606  pcpremul  12616  pcdvdsb  12643  dvdsprmpweqnn  12659  dvdsprmpweqle  12660  difsqpwdvds  12661  pcfaclem  12672  pcbc  12674  4sqlem12  12725  unennn  12768  nninfdc  12824  setsex  12864  f1ocpbllem  13142  imasaddfnlemg  13146  imasaddvallemg  13147  ercpbl  13163  erlecpbl  13164  qusaddvallemg  13165  fvprif  13175  xpsfrnel2  13178  plusfvalg  13195  imasmnd  13285  insubm  13317  grpidrcan  13397  grpidlcan  13398  grpsubpropd2  13437  pwsinvg  13444  imasgrp2  13446  imasgrp  13447  mulgnnsubcl  13470  mulgnn0subcl  13471  mulgsubcl  13472  mulgaddcom  13482  mulginvcom  13483  mulgnnass  13493  mulgassr  13496  mulgpropdg  13500  submmulg  13502  subgcl  13520  subgsubcl  13521  subgsub  13522  subgmulg  13524  nsgconj  13542  ghmsub  13587  ghmrn  13593  ghmeqker  13607  f1ghm0to0  13608  ablinvadd  13646  ablsub4  13649  abladdsub4  13650  subcmnd  13669  imasabl  13672  rngcl  13706  imasrng  13718  srgcl  13732  srg1zr  13749  srgen1zr  13750  ringcl  13775  crngcom  13776  ringidss  13791  mulgass2  13820  imasring  13826  opprmulg  13833  unitmulclb  13876  unitdvcl  13898  rhmmul  13926  rhmdvdsr  13937  subrngmcl  13971  subrgmcl  13995  subrgdv  14000  subrgugrp  14002  domneq0  14034  scafvalg  14069  lmodprop2d  14110  lssclg  14126  lssvnegcl  14138  lssintclm  14146  sralmod  14212  rnglidlmcl  14242  lidlnegcl  14247  rspssp  14256  rnglidlmsgrp  14259  rnglidlrng  14260  2idlcpblrng  14285  qus2idrng  14287  zndvds  14411  znleval2  14416  basgen  14552  2basgeng  14554  iuncld  14587  neipsm  14626  opnneissb  14627  opnssneib  14628  iscnp3  14675  cnprcl2k  14678  cnpnei  14691  cncnp2m  14703  cnptoprest  14711  sslm  14719  upxp  14744  cnmpt22  14766  distspace  14807  0met  14856  blvalps  14860  blval  14861  ssblps  14897  ssbl  14898  blpnfctr  14911  blopn  14962  blnei  14964  bdxmet  14973  bdbl  14975  metcnp3  14983  tgqioo  15027  ptolemy  15296  sinq12gt0  15302  sincosq1eq  15311  rpcxpadd  15377  cxpmul  15384  rplogbval  15417  logbleb  15433  logbgcd1irr  15439  logbprmirr  15444  lgsfvalg  15482  lgsneg1  15502  lgssq  15517  lgsdinn0  15525  gausslemma2dlem1a  15535  2lgs  15581  2lgsoddprmlem2  15583  funvtxdm2domval  15626  funiedgdm2domval  15627  bdfind  15882  1dom1el  15927