Theorem 3ad2ant1 1045

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  simp1l  1048  simp1r  1049  simp11  1054  simp12  1055  simp13  1056  simp1ll  1087  simp1lr  1088  simp1rl  1089  simp1rr  1090  simp1l1  1117  simp1l2  1118  simp1l3  1119  simp1r1  1120  simp1r2  1121  simp1r3  1122  simp11l  1135  simp11r  1136  simp12l  1137  simp12r  1138  simp13l  1139  simp13r  1140  simp111  1153  simp112  1154  simp113  1155  simp121  1156  simp122  1157  simp123  1158  simp131  1159  simp132  1160  simp133  1161  3anim123i  1211  3jaao  1345  ceqsalt  2830  sbciegft  3063  reupick2  3495  ifbothdc  3644  frirrg  4453  breldmg  4943  fntpg  5393  funimaexglem  5420  fex2  5511  fvun1  5721  fprg  5845  fsnunfv  5863  fnfvima  5899  cocan1  5938  cocan2  5939  mpoeq3dv  6097  fovcld  6136  fvmpopr2d  6168  funexw  6283  mpofvex  6379  poxp  6406  suppval1  6417  suppvalfng  6418  suppvalfn  6419  suppimacnvfn  6424  suppsnopdc  6428  smoiso  6511  tfrlem5  6523  tfrlemibxssdm  6536  tfr1onlembfn  6553  tfri1dALT  6560  tfrcllembfn  6566  rdgon  6595  freccllem  6611  nnawordex  6740  1dom1el  7036  mapxpen  7077  fidceq  7099  fidifsnen  7100  dif1en  7111  en2eqpr  7142  unsnfi  7154  unsnfidcex  7155  unsnfidcel  7156  fisseneq  7170  ordiso2  7277  updjud  7324  mkvprop  7400  endjudisj  7468  xpdjuen  7476  mulcanenq0ec  7708  prltlu  7750  prarloclem3step  7759  prarloclem5  7763  ltasrg  8033  cnegexlem1  8396  addcan  8401  apcotr  8829  apadd1  8830  mulext1  8834  divdivap1  8945  divdivap2  8946  div2negap  8957  divneg2ap  8958  ltmulgt11  9086  ltdiv2  9109  squeeze0  9126  nndivtr  9227  nn0n0n1ge2  9594  zdivmul  9614  gtndiv  9619  eluzuzle  9808  eluzp1p1  9826  qdivcl  9921  irrmul  9925  rpgecl  9961  xaddass  10148  xltadd1  10155  xlt2add  10159  lbico1  10209  lbicc2  10263  zltaddlt1le  10287  uzsubsubfz  10327  elfz1b  10370  elfz0ubfz0  10405  fz0fzelfz0  10407  difelfzle  10414  difelfznle  10415  2ffzeq  10421  fzo1fzo0n0  10468  ubmelfzo  10491  fzonn0p1p1  10504  elfzom1p1elfzo  10505  elfzonelfzo  10521  subfzo0  10534  ceiqle  10621  ceilqle  10622  modqval  10632  flqpmodeq  10635  modq0  10637  negqmod0  10639  modqge0  10640  modqlt  10641  modqdiffl  10643  modqmulnn  10650  modqvalp1  10651  modqmuladdnn0  10676  qnegmod  10677  addmodid  10680  modfzo0difsn  10703  addmodlteq  10706  qexpclz  10868  expgt1  10885  expp1zap  10896  expm1ap  10897  expubnd  10904  bernneq2  10969  expnlbnd  10972  mulsubdivbinom2ap  11019  omgadd  11111  hashun  11114  fihashssdif  11128  hashdifpr  11130  fimaxq  11137  ccatval2  11224  ccatval3  11225  ccatval1lsw  11230  ccatval21sw  11231  ccatass  11234  ccatw2s1leng  11264  ccats1val2  11266  ccat2s1fvwd  11273  fzowrddc  11277  swrdval  11278  swrdclg  11280  swrdval2  11281  swrdnd  11289  swrdlen2  11292  swrdfv2  11293  ccatswrd  11300  pfxn0  11318  pfxsuff1eqwrdeq  11329  swrdswrdlem  11334  ccats1pfxeq  11344  ccats1pfxeqrex  11345  ccatopth2  11347  wrd2ind  11353  pfxccatin12lem3  11362  pfxccat3  11364  swrdccat  11365  pfxccatpfx2  11367  pfxccat3a  11368  swrdccat3b  11370  pfxccatid  11371  ccats1pfxeqbi  11372  shftuz  11440  mulreap  11487  redivap  11497  imdivap  11504  resqrtcl  11652  xrmaxltsup  11881  xrmaxaddlem  11883  xrmaxadd  11884  xrlemininf  11894  xrminltinf  11895  climuni  11916  addcn2  11933  mulcn2  11935  efsub  12305  sin02gt0  12388  cos12dec  12392  dvdsval2  12414  addmodlteqALT  12483  modremain  12553  fldivndvdslt  12561  mulgcdr  12652  gcddiv  12653  rpmulgcd  12660  rplpwr  12661  rppwr  12662  nnminle  12669  qredeq  12731  divgcdcoprmex  12737  cncongr1  12738  cncongr2  12739  dvdsnprmd  12760  euclemma  12781  prmexpb  12786  qnumdenbi  12827  eulerth  12868  fermltl  12869  prmdiv  12870  hashgcdlem  12873  odzcllem  12878  vfermltl  12887  reumodprminv  12889  modprm0  12890  modprmn0modprm0  12892  coprimeprodsq  12893  pythagtriplem1  12901  pythagtriplem3  12903  pythagtriplem4  12904  pythagtriplem10  12905  pythagtriplem6  12906  pythagtriplem7  12907  pythagtriplem8  12908  pythagtriplem9  12909  pythagtriplem11  12910  pythagtriplem12  12911  pythagtriplem13  12912  pythagtriplem14  12913  pythagtriplem15  12914  pythagtriplem16  12915  pythagtriplem17  12916  pythagtriplem19  12918  pythagtrip  12919  pcpremul  12929  pcdvdsb  12956  dvdsprmpweqnn  12972  dvdsprmpweqle  12973  difsqpwdvds  12974  pcfaclem  12985  pcbc  12987  4sqlem12  13038  unennn  13081  nninfdc  13137  setsex  13177  f1ocpbllem  13456  imasaddfnlemg  13460  imasaddvallemg  13461  ercpbl  13477  erlecpbl  13478  qusaddvallemg  13479  fvprif  13489  xpsfrnel2  13492  plusfvalg  13509  imasmnd  13599  insubm  13631  grpidrcan  13711  grpidlcan  13712  grpsubpropd2  13751  pwsinvg  13758  imasgrp2  13760  imasgrp  13761  mulgnnsubcl  13784  mulgnn0subcl  13785  mulgsubcl  13786  mulgaddcom  13796  mulginvcom  13797  mulgnnass  13807  mulgassr  13810  mulgpropdg  13814  submmulg  13816  subgcl  13834  subgsubcl  13835  subgsub  13836  subgmulg  13838  nsgconj  13856  ghmsub  13901  ghmrn  13907  ghmeqker  13921  f1ghm0to0  13922  ablinvadd  13960  ablsub4  13963  abladdsub4  13964  subcmnd  13983  imasabl  13986  rngcl  14021  imasrng  14033  srgcl  14047  srg1zr  14064  srgen1zr  14065  ringcl  14090  crngcom  14091  ringidss  14106  mulgass2  14135  imasring  14141  opprmulg  14148  unitmulclb  14192  unitdvcl  14214  rhmmul  14242  rhmdvdsr  14253  subrngmcl  14287  subrgmcl  14311  subrgdv  14316  subrgugrp  14318  domneq0  14351  scafvalg  14386  lmodprop2d  14427  lssclg  14443  lssvnegcl  14455  lssintclm  14463  sralmod  14529  rnglidlmcl  14559  lidlnegcl  14564  rspssp  14573  rnglidlmsgrp  14576  rnglidlrng  14577  2idlcpblrng  14602  qus2idrng  14604  zndvds  14728  znleval2  14733  psrbaglesupp  14752  psrbaglecl  14754  psrbagcon  14755  basgen  14874  2basgeng  14876  iuncld  14909  neipsm  14948  opnneissb  14949  opnssneib  14950  iscnp3  14997  cnprcl2k  15000  cnpnei  15013  cncnp2m  15025  cnptoprest  15033  sslm  15041  upxp  15066  cnmpt22  15088  distspace  15129  0met  15178  blvalps  15182  blval  15183  ssblps  15219  ssbl  15220  blpnfctr  15233  blopn  15284  blnei  15286  bdxmet  15295  bdbl  15297  metcnp3  15305  tgqioo  15349  ptolemy  15618  sinq12gt0  15624  sincosq1eq  15633  rpcxpadd  15699  cxpmul  15706  rplogbval  15739  logbleb  15755  logbgcd1irr  15761  logbprmirr  15766  pellexlem1  15774  lgsfvalg  15807  lgsneg1  15827  lgssq  15842  lgsdinn0  15850  gausslemma2dlem1a  15860  2lgs  15906  2lgsoddprmlem2  15908  funvtxdm2domval  15953  funiedgdm2domval  15954  iedgedgg  15985  lpvtx  16003  incistruhgr  16014  ausgrumgrien  16094  ausgrusgrien  16095  umgr2edgneu  16136  ushgredgedg  16150  ushgredgedgloop  16152  usgr2v1e2w  16170  egrsubgr  16187  subumgredg2en  16195  iswlk  16247  wlkl1loop  16282  uspgr2wlkeq  16289  istrl  16309  clwwlkccatlem  16324  clwwlkccat  16325  clwwlknccat  16347  clwwlknonex2lem2  16362  clwwlknonex2  16363  iseupth  16371  eupth2lem3lem6fi  16395  konigsbergssiedgwen  16410  bdfind  16645  repiecele0  16741  repiecege0  16742