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  2800  sbciegft  3033  reupick2  3463  ifbothdc  3610  frirrg  4410  breldmg  4898  fntpg  5344  funimaexglem  5371  fex2  5459  fvun1  5663  fprg  5785  fsnunfv  5803  fnfvima  5837  cocan1  5874  cocan2  5875  mpoeq3dv  6029  fovcld  6068  fvmpopr2d  6100  funexw  6215  mpofvex  6309  poxp  6336  smoiso  6406  tfrlem5  6418  tfrlemibxssdm  6431  tfr1onlembfn  6448  tfri1dALT  6455  tfrcllembfn  6461  rdgon  6490  freccllem  6506  nnawordex  6633  mapxpen  6965  fidceq  6987  fidifsnen  6988  dif1en  6997  en2eqpr  7025  unsnfi  7037  unsnfidcex  7038  unsnfidcel  7039  fisseneq  7052  ordiso2  7158  updjud  7205  mkvprop  7281  endjudisj  7348  xpdjuen  7356  mulcanenq0ec  7588  prltlu  7630  prarloclem3step  7639  prarloclem5  7643  ltasrg  7913  cnegexlem1  8277  addcan  8282  apcotr  8710  apadd1  8711  mulext1  8715  divdivap1  8826  divdivap2  8827  div2negap  8838  divneg2ap  8839  ltmulgt11  8967  ltdiv2  8990  squeeze0  9007  nndivtr  9108  nn0n0n1ge2  9473  zdivmul  9493  gtndiv  9498  eluzuzle  9686  eluzp1p1  9704  qdivcl  9794  irrmul  9798  rpgecl  9834  xaddass  10021  xltadd1  10028  xlt2add  10032  lbico1  10082  lbicc2  10136  zltaddlt1le  10159  uzsubsubfz  10199  elfz1b  10242  elfz0ubfz0  10277  fz0fzelfz0  10279  difelfzle  10286  difelfznle  10287  2ffzeq  10293  fzo1fzo0n0  10339  ubmelfzo  10361  fzonn0p1p1  10374  elfzom1p1elfzo  10375  elfzonelfzo  10391  subfzo0  10403  ceiqle  10490  ceilqle  10491  modqval  10501  flqpmodeq  10504  modq0  10506  negqmod0  10508  modqge0  10509  modqlt  10510  modqdiffl  10512  modqmulnn  10519  modqvalp1  10520  modqmuladdnn0  10545  qnegmod  10546  addmodid  10549  modfzo0difsn  10572  addmodlteq  10575  qexpclz  10737  expgt1  10754  expp1zap  10765  expm1ap  10766  expubnd  10773  bernneq2  10838  expnlbnd  10841  mulsubdivbinom2ap  10888  omgadd  10979  hashun  10982  fihashssdif  10995  hashdifpr  10997  fimaxq  11004  ccatval2  11087  ccatval3  11088  ccatval1lsw  11093  ccatval21sw  11094  ccatass  11097  ccats1val2  11125  fzowrddc  11133  swrdval  11134  swrdclg  11136  swrdval2  11137  swrdnd  11145  swrdlen2  11148  swrdfv2  11149  ccatswrd  11156  pfxn0  11174  pfxsuff1eqwrdeq  11185  swrdswrdlem  11190  ccats1pfxeq  11200  ccats1pfxeqrex  11201  ccatopth2  11203  wrd2ind  11209  shftuz  11213  mulreap  11260  redivap  11270  imdivap  11277  resqrtcl  11425  xrmaxltsup  11654  xrmaxaddlem  11656  xrmaxadd  11657  xrlemininf  11667  xrminltinf  11668  climuni  11689  addcn2  11706  mulcn2  11708  efsub  12077  sin02gt0  12160  cos12dec  12164  dvdsval2  12186  addmodlteqALT  12255  modremain  12325  fldivndvdslt  12333  mulgcdr  12424  gcddiv  12425  rpmulgcd  12432  rplpwr  12433  rppwr  12434  nnminle  12441  qredeq  12503  divgcdcoprmex  12509  cncongr1  12510  cncongr2  12511  dvdsnprmd  12532  euclemma  12553  prmexpb  12558  qnumdenbi  12599  eulerth  12640  fermltl  12641  prmdiv  12642  hashgcdlem  12645  odzcllem  12650  vfermltl  12659  reumodprminv  12661  modprm0  12662  modprmn0modprm0  12664  coprimeprodsq  12665  pythagtriplem1  12673  pythagtriplem3  12675  pythagtriplem4  12676  pythagtriplem10  12677  pythagtriplem6  12678  pythagtriplem7  12679  pythagtriplem8  12680  pythagtriplem9  12681  pythagtriplem11  12682  pythagtriplem12  12683  pythagtriplem13  12684  pythagtriplem14  12685  pythagtriplem15  12686  pythagtriplem16  12687  pythagtriplem17  12688  pythagtriplem19  12690  pythagtrip  12691  pcpremul  12701  pcdvdsb  12728  dvdsprmpweqnn  12744  dvdsprmpweqle  12745  difsqpwdvds  12746  pcfaclem  12757  pcbc  12759  4sqlem12  12810  unennn  12853  nninfdc  12909  setsex  12949  f1ocpbllem  13227  imasaddfnlemg  13231  imasaddvallemg  13232  ercpbl  13248  erlecpbl  13249  qusaddvallemg  13250  fvprif  13260  xpsfrnel2  13263  plusfvalg  13280  imasmnd  13370  insubm  13402  grpidrcan  13482  grpidlcan  13483  grpsubpropd2  13522  pwsinvg  13529  imasgrp2  13531  imasgrp  13532  mulgnnsubcl  13555  mulgnn0subcl  13556  mulgsubcl  13557  mulgaddcom  13567  mulginvcom  13568  mulgnnass  13578  mulgassr  13581  mulgpropdg  13585  submmulg  13587  subgcl  13605  subgsubcl  13606  subgsub  13607  subgmulg  13609  nsgconj  13627  ghmsub  13672  ghmrn  13678  ghmeqker  13692  f1ghm0to0  13693  ablinvadd  13731  ablsub4  13734  abladdsub4  13735  subcmnd  13754  imasabl  13757  rngcl  13791  imasrng  13803  srgcl  13817  srg1zr  13834  srgen1zr  13835  ringcl  13860  crngcom  13861  ringidss  13876  mulgass2  13905  imasring  13911  opprmulg  13918  unitmulclb  13961  unitdvcl  13983  rhmmul  14011  rhmdvdsr  14022  subrngmcl  14056  subrgmcl  14080  subrgdv  14085  subrgugrp  14087  domneq0  14119  scafvalg  14154  lmodprop2d  14195  lssclg  14211  lssvnegcl  14223  lssintclm  14231  sralmod  14297  rnglidlmcl  14327  lidlnegcl  14332  rspssp  14341  rnglidlmsgrp  14344  rnglidlrng  14345  2idlcpblrng  14370  qus2idrng  14372  zndvds  14496  znleval2  14501  basgen  14637  2basgeng  14639  iuncld  14672  neipsm  14711  opnneissb  14712  opnssneib  14713  iscnp3  14760  cnprcl2k  14763  cnpnei  14776  cncnp2m  14788  cnptoprest  14796  sslm  14804  upxp  14829  cnmpt22  14851  distspace  14892  0met  14941  blvalps  14945  blval  14946  ssblps  14982  ssbl  14983  blpnfctr  14996  blopn  15047  blnei  15049  bdxmet  15058  bdbl  15060  metcnp3  15068  tgqioo  15112  ptolemy  15381  sinq12gt0  15387  sincosq1eq  15396  rpcxpadd  15462  cxpmul  15469  rplogbval  15502  logbleb  15518  logbgcd1irr  15524  logbprmirr  15529  lgsfvalg  15567  lgsneg1  15587  lgssq  15602  lgsdinn0  15610  gausslemma2dlem1a  15620  2lgs  15666  2lgsoddprmlem2  15668  funvtxdm2domval  15713  funiedgdm2domval  15714  iedgedgg  15742  lpvtx  15760  incistruhgr  15771  bdfind  16051  1dom1el  16096