Theorem 3ad2ant1 1020

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  simp1l  1023  simp1r  1024  simp11  1029  simp12  1030  simp13  1031  simp1ll  1062  simp1lr  1063  simp1rl  1064  simp1rr  1065  simp1l1  1092  simp1l2  1093  simp1l3  1094  simp1r1  1095  simp1r2  1096  simp1r3  1097  simp11l  1110  simp11r  1111  simp12l  1112  simp12r  1113  simp13l  1114  simp13r  1115  simp111  1128  simp112  1129  simp113  1130  simp121  1131  simp122  1132  simp123  1133  simp131  1134  simp132  1135  simp133  1136  3anim123i  1186  3jaao  1320  ceqsalt  2797  sbciegft  3028  reupick2  3458  ifbothdc  3604  frirrg  4396  breldmg  4883  fntpg  5329  funimaexglem  5356  fex2  5443  fvun1  5644  fprg  5766  fsnunfv  5784  fnfvima  5818  cocan1  5855  cocan2  5856  mpoeq3dv  6010  fovcld  6049  fvmpopr2d  6081  funexw  6196  mpofvex  6290  poxp  6317  smoiso  6387  tfrlem5  6399  tfrlemibxssdm  6412  tfr1onlembfn  6429  tfri1dALT  6436  tfrcllembfn  6442  rdgon  6471  freccllem  6487  nnawordex  6614  mapxpen  6944  fidceq  6965  fidifsnen  6966  dif1en  6975  en2eqpr  7003  unsnfi  7015  unsnfidcex  7016  unsnfidcel  7017  fisseneq  7030  ordiso2  7136  updjud  7183  mkvprop  7259  endjudisj  7321  xpdjuen  7329  mulcanenq0ec  7557  prltlu  7599  prarloclem3step  7608  prarloclem5  7612  ltasrg  7882  cnegexlem1  8246  addcan  8251  apcotr  8679  apadd1  8680  mulext1  8684  divdivap1  8795  divdivap2  8796  div2negap  8807  divneg2ap  8808  ltmulgt11  8936  ltdiv2  8959  squeeze0  8976  nndivtr  9077  nn0n0n1ge2  9442  zdivmul  9462  gtndiv  9467  eluzuzle  9655  eluzp1p1  9673  qdivcl  9763  irrmul  9767  rpgecl  9803  xaddass  9990  xltadd1  9997  xlt2add  10001  lbico1  10051  lbicc2  10105  zltaddlt1le  10128  uzsubsubfz  10168  elfz1b  10211  elfz0ubfz0  10246  fz0fzelfz0  10248  difelfzle  10255  difelfznle  10256  2ffzeq  10262  fzo1fzo0n0  10305  ubmelfzo  10327  fzonn0p1p1  10340  elfzom1p1elfzo  10341  elfzonelfzo  10357  subfzo0  10369  ceiqle  10456  ceilqle  10457  modqval  10467  flqpmodeq  10470  modq0  10472  negqmod0  10474  modqge0  10475  modqlt  10476  modqdiffl  10478  modqmulnn  10485  modqvalp1  10486  modqmuladdnn0  10511  qnegmod  10512  addmodid  10515  modfzo0difsn  10538  addmodlteq  10541  qexpclz  10703  expgt1  10720  expp1zap  10731  expm1ap  10732  expubnd  10739  bernneq2  10804  expnlbnd  10807  mulsubdivbinom2ap  10854  omgadd  10945  hashun  10948  fihashssdif  10961  hashdifpr  10963  fimaxq  10970  ccatval2  11052  ccatval3  11053  ccatval1lsw  11058  ccatval21sw  11059  ccatass  11062  shftuz  11070  mulreap  11117  redivap  11127  imdivap  11134  resqrtcl  11282  xrmaxltsup  11511  xrmaxaddlem  11513  xrmaxadd  11514  xrlemininf  11524  xrminltinf  11525  climuni  11546  addcn2  11563  mulcn2  11565  efsub  11934  sin02gt0  12017  cos12dec  12021  dvdsval2  12043  addmodlteqALT  12112  modremain  12182  fldivndvdslt  12190  mulgcdr  12281  gcddiv  12282  rpmulgcd  12289  rplpwr  12290  rppwr  12291  nnminle  12298  qredeq  12360  divgcdcoprmex  12366  cncongr1  12367  cncongr2  12368  dvdsnprmd  12389  euclemma  12410  prmexpb  12415  qnumdenbi  12456  eulerth  12497  fermltl  12498  prmdiv  12499  hashgcdlem  12502  odzcllem  12507  vfermltl  12516  reumodprminv  12518  modprm0  12519  modprmn0modprm0  12521  coprimeprodsq  12522  pythagtriplem1  12530  pythagtriplem3  12532  pythagtriplem4  12533  pythagtriplem10  12534  pythagtriplem6  12535  pythagtriplem7  12536  pythagtriplem8  12537  pythagtriplem9  12538  pythagtriplem11  12539  pythagtriplem12  12540  pythagtriplem13  12541  pythagtriplem14  12542  pythagtriplem15  12543  pythagtriplem16  12544  pythagtriplem17  12545  pythagtriplem19  12547  pythagtrip  12548  pcpremul  12558  pcdvdsb  12585  dvdsprmpweqnn  12601  dvdsprmpweqle  12602  difsqpwdvds  12603  pcfaclem  12614  pcbc  12616  4sqlem12  12667  unennn  12710  nninfdc  12766  setsex  12806  f1ocpbllem  13084  imasaddfnlemg  13088  imasaddvallemg  13089  ercpbl  13105  erlecpbl  13106  qusaddvallemg  13107  fvprif  13117  xpsfrnel2  13120  plusfvalg  13137  imasmnd  13227  insubm  13259  grpidrcan  13339  grpidlcan  13340  grpsubpropd2  13379  pwsinvg  13386  imasgrp2  13388  imasgrp  13389  mulgnnsubcl  13412  mulgnn0subcl  13413  mulgsubcl  13414  mulgaddcom  13424  mulginvcom  13425  mulgnnass  13435  mulgassr  13438  mulgpropdg  13442  submmulg  13444  subgcl  13462  subgsubcl  13463  subgsub  13464  subgmulg  13466  nsgconj  13484  ghmsub  13529  ghmrn  13535  ghmeqker  13549  f1ghm0to0  13550  ablinvadd  13588  ablsub4  13591  abladdsub4  13592  subcmnd  13611  imasabl  13614  rngcl  13648  imasrng  13660  srgcl  13674  srg1zr  13691  srgen1zr  13692  ringcl  13717  crngcom  13718  ringidss  13733  mulgass2  13762  imasring  13768  opprmulg  13775  unitmulclb  13818  unitdvcl  13840  rhmmul  13868  rhmdvdsr  13879  subrngmcl  13913  subrgmcl  13937  subrgdv  13942  subrgugrp  13944  domneq0  13976  scafvalg  14011  lmodprop2d  14052  lssclg  14068  lssvnegcl  14080  lssintclm  14088  sralmod  14154  rnglidlmcl  14184  lidlnegcl  14189  rspssp  14198  rnglidlmsgrp  14201  rnglidlrng  14202  2idlcpblrng  14227  qus2idrng  14229  zndvds  14353  znleval2  14358  basgen  14494  2basgeng  14496  iuncld  14529  neipsm  14568  opnneissb  14569  opnssneib  14570  iscnp3  14617  cnprcl2k  14620  cnpnei  14633  cncnp2m  14645  cnptoprest  14653  sslm  14661  upxp  14686  cnmpt22  14708  distspace  14749  0met  14798  blvalps  14802  blval  14803  ssblps  14839  ssbl  14840  blpnfctr  14853  blopn  14904  blnei  14906  bdxmet  14915  bdbl  14917  metcnp3  14925  tgqioo  14969  ptolemy  15238  sinq12gt0  15244  sincosq1eq  15253  rpcxpadd  15319  cxpmul  15326  rplogbval  15359  logbleb  15375  logbgcd1irr  15381  logbprmirr  15386  lgsfvalg  15424  lgsneg1  15444  lgssq  15459  lgsdinn0  15467  gausslemma2dlem1a  15477  2lgs  15523  2lgsoddprmlem2  15525  funvtxdm2domval  15568  funiedgdm2domval  15569  bdfind  15815  1dom1el  15860