Theorem 3ad2ant1 1049

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simp1l  1052  simp1r  1053  simp11  1058  simp12  1059  simp13  1060  simp1ll  1091  simp1lr  1092  simp1rl  1093  simp1rr  1094  simp1l1  1121  simp1l2  1122  simp1l3  1123  simp1r1  1124  simp1r2  1125  simp1r3  1126  simp11l  1139  simp11r  1140  simp12l  1141  simp12r  1142  simp13l  1143  simp13r  1144  simp111  1157  simp112  1158  simp113  1159  simp121  1160  simp122  1161  simp123  1162  simp131  1163  simp132  1164  simp133  1165  3anim123i  1215  3jaao  1349  ceqsalt  2848  sbciegft  3082  reupick2  3519  ifbothdc  3675  ifprdc  3819  frirrg  4495  breldmg  4987  fntpg  5437  funimaexglem  5464  fex2  5556  fresaunres2disj  5570  fvun1  5769  fprg  5898  fsnunfv  5916  fnfvima  5953  cocan1  5993  cocan2  5994  mpoeq3dv  6154  fovcld  6193  fvmpopr2d  6225  funexw  6341  mpofvex  6441  poxp  6468  suppval1  6479  suppvalfng  6480  suppvalfn  6481  suppimacnvfn  6486  suppsnopdc  6490  smoiso  6573  tfrlem5  6585  tfrlemibxssdm  6598  tfr1onlembfn  6615  tfri1dALT  6622  tfrcllembfn  6628  rdgon  6657  freccllem  6673  nnawordex  6802  1dom1el  7107  mapxpen  7148  fidceq  7171  fidifsnen  7172  dif1en  7183  en2eqpr  7214  unsnfi  7226  unsnfidcex  7227  unsnfidcel  7228  fisseneq  7242  funisfsupp  7291  ordiso2  7376  updjud  7423  mkvprop  7499  endjudisj  7567  xpdjuen  7575  mulcanenq0ec  7813  prltlu  7855  prarloclem3step  7864  prarloclem5  7868  ltasrg  8138  cnegexlem1  8503  addcan  8508  apcotr  8938  apadd1  8939  mulext1  8943  divdivap1  9056  divdivap2  9057  div2negap  9068  divneg2ap  9069  ltmulgt11  9197  ltdiv2  9220  squeeze0  9237  nndivtr  9349  nn0n0n1ge2  9720  zdivmul  9741  gtndiv  9746  eluzuzle  9940  eluzp1p1  9958  qdivcl  10053  irrmul  10058  rpgecl  10094  xaddass  10282  xltadd1  10289  xlt2add  10293  lbico1  10343  lbicc2  10397  zltaddlt1le  10421  uzsubsubfz  10463  elfz1b  10508  elfz0ubfz0  10543  fz0fzelfz0  10545  difelfzle  10552  difelfznle  10553  2ffzeq  10559  fzo1fzo0n0  10606  ubmelfzo  10629  fzonn0p1p1  10642  elfzom1p1elfzo  10643  elfzonelfzo  10659  subfzo0  10672  ceiqle  10765  ceilqle  10766  modqval  10776  flqpmodeq  10779  modq0  10781  negqmod0  10783  modqge0  10784  modqlt  10785  modqdiffl  10787  modqmulnn  10794  modqvalp1  10795  modqmuladdnn0  10820  qnegmod  10821  addmodid  10824  modfzo0difsn  10847  addmodlteq  10850  qexpclz  11012  expgt1  11029  expp1zap  11040  expm1ap  11041  expubnd  11048  bernneq2  11114  expnlbnd  11117  mulsubdivbinom2ap  11165  omgadd  11258  hashun  11261  fihashssdif  11275  hashdifpr  11277  fimaxq  11286  ccatval2  11382  ccatval3  11383  ccatval1lsw  11388  ccatval21sw  11389  ccatass  11392  ccatw2s1leng  11422  ccats1val2  11424  ccat2s1fvwd  11431  fzowrddc  11435  swrdval  11436  swrdclg  11438  swrdval2  11439  swrdnd  11447  swrdlen2  11450  swrdfv2  11451  ccatswrd  11458  pfxn0  11476  pfxsuff1eqwrdeq  11487  swrdswrdlem  11492  ccats1pfxeq  11502  ccats1pfxeqrex  11503  ccatopth2  11505  wrd2ind  11511  pfxccatin12lem3  11520  pfxccat3  11522  swrdccat  11523  pfxccatpfx2  11525  pfxccat3a  11526  swrdccat3b  11528  pfxccatid  11529  ccats1pfxeqbi  11530  shftuz  11598  mulreap  11645  redivap  11655  imdivap  11662  resqrtcl  11811  xrmaxltsup  12043  xrmaxaddlem  12045  xrmaxadd  12046  xrlemininf  12056  xrminltinf  12057  climuni  12078  addcn2  12095  mulcn2  12097  efsub  12467  sin02gt0  12550  cos12dec  12554  dvdsval2  12576  addmodlteqALT  12645  modremain  12715  fldivndvdslt  12723  mulgcdr  12814  gcddiv  12815  rpmulgcd  12822  rplpwr  12823  rppwr  12824  nnminle  12831  qredeq  12893  divgcdcoprmex  12899  cncongr1  12900  cncongr2  12901  dvdsnprmd  12922  euclemma  12944  prmexpb  12949  qnumdenbi  12991  eulerth  13034  fermltl  13035  prmdiv  13036  hashgcdlem  13039  odzcllem  13044  vfermltl  13053  reumodprminv  13055  modprm0  13056  modprmn0modprm0  13058  coprimeprodsq  13059  pythagtriplem1  13067  pythagtriplem3  13069  pythagtriplem4  13070  pythagtriplem10  13071  pythagtriplem6  13072  pythagtriplem7  13073  pythagtriplem8  13074  pythagtriplem9  13075  pythagtriplem11  13076  pythagtriplem12  13077  pythagtriplem13  13078  pythagtriplem14  13079  pythagtriplem15  13080  pythagtriplem16  13081  pythagtriplem17  13082  pythagtriplem19  13084  pythagtrip  13085  pcpremul  13095  pcdvdsb  13122  dvdsprmpweqnn  13138  dvdsprmpweqle  13139  difsqpwdvds  13140  pcfaclem  13151  pcbc  13153  4sqlem12  13204  ballotfilemsgt1  13306  ballotfilemieq  13312  ballotfilemfrcn0  13325  unennn  13340  nninfdc  13396  setsex  13436  f1ocpbllem  13684  imasaddfnlemg  13688  imasaddvallemg  13689  ercpbl  13705  erlecpbl  13706  qusaddvallemg  13707  fvprif  13717  xpsfrnel2  13720  plusfvalg  13736  imasmnd  13813  insubm  13845  grpidrcan  13923  grpidlcan  13924  grpsubpropd2  13963  imasgrp2  13966  imasgrp  13967  mulgnnsubcl  13990  mulgnn0subcl  13991  mulgsubcl  13992  mulgaddcom  14002  mulginvcom  14003  mulgnnass  14013  mulgassr  14016  mulgpropdg  14020  submmulg  14022  subgcl  14040  subgsubcl  14041  subgsub  14042  subgmulg  14044  nsgconj  14062  ghmsub  14107  ghmrn  14113  ghmeqker  14127  f1ghm0to0  14128  ablinvadd  14198  ablsub4  14201  abladdsub4  14202  subcmnd  14221  imasabl  14224  gsumconstcmn  14250  pwsinvg  14299  rngcl  14327  imasrng  14339  rng1zrlem  14342  rng1zr  14343  rngen1zr0  14345  srgcl  14358  srg1zr  14375  srgen1zr0  14376  ringcl  14401  crngcom  14402  ringidss  14418  mulgass2  14447  imasring  14453  opprmulg  14460  unitmulclb  14505  unitdvcl  14527  rhmmul  14555  rhmdvdsr  14566  subrngmcl  14601  subrgmcl  14625  subrgdv  14630  subrgugrp  14632  domneq0  14665  scafvalg  14728  lmodprop2d  14769  lssclg  14785  lssvnegcl  14797  lssintclm  14805  sralmod  14871  rnglidlmcl  14901  lidlnegcl  14906  rspssp  14915  rnglidlmsgrp  14918  rnglidlrng  14919  2idlcpblrng  14944  qus2idrng  14946  zndvds  15068  znleval2  15073  assa2ass  15093  assa2ass2  15094  asclmul1  15113  asclmul2  15114  ascldimul  15115  asclmulg  15128  psrbaglesupp  15142  psrbaglecl  15144  psrbagaddclfi  15145  psrbagcon  15146  basgen  15272  2basgeng  15274  iuncld  15307  neipsm  15346  opnneissb  15347  opnssneib  15348  iscnp3  15395  cnprcl2k  15398  cnpnei  15411  cncnp2m  15423  cnptoprest  15431  sslm  15439  upxp  15464  cnmpt22  15486  distspace  15527  0met  15576  blvalps  15580  blval  15581  ssblps  15617  ssbl  15618  blpnfctr  15631  blopn  15682  blnei  15684  bdxmet  15693  bdbl  15695  metcnp3  15703  tgqioo  15747  ptolemy  16017  sinq12gt0  16023  sincosq1eq  16032  rpcxpadd  16102  cxpmul  16109  rplogbval  16142  logbleb  16158  logbgcd1irr  16164  logbprmirr  16169  pellexlem1  16190  chtqwordi  16224  efchtqdvds  16226  ppiqwordi  16229  bcmono  16265  lgsfvalg  16290  lgsneg1  16310  lgssq  16325  lgsdinn0  16333  gausslemma2dlem1a  16343  2lgs  16389  2lgsoddprmlem2  16391  funvtxdm2domval  16436  funiedgdm2domval  16437  iedgedgg  16468  lpvtx  16486  incistruhgr  16497  ausgrumgrien  16577  ausgrusgrien  16578  umgr2edgneu  16619  ushgredgedg  16633  ushgredgedgloop  16635  usgr2v1e2w  16653  egrsubgr  16670  subumgredg2en  16678  iswlk  16730  wlkl1loop  16765  uspgr2wlkeq  16772  istrl  16792  clwwlkccatlem  16807  clwwlkccat  16808  clwwlknccat  16830  clwwlknonex2lem2  16845  clwwlknonex2  16846  iseupth  16854  eupth2lem3lem6fi  16878  konigsbergssiedgwen  16893  bdfind  17138  repiecele0  17241  repiecege0  17242