Theorem 3ad2ant1 1044

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  simp1l  1047  simp1r  1048  simp11  1053  simp12  1054  simp13  1055  simp1ll  1086  simp1lr  1087  simp1rl  1088  simp1rr  1089  simp1l1  1116  simp1l2  1117  simp1l3  1118  simp1r1  1119  simp1r2  1120  simp1r3  1121  simp11l  1134  simp11r  1135  simp12l  1136  simp12r  1137  simp13l  1138  simp13r  1139  simp111  1152  simp112  1153  simp113  1154  simp121  1155  simp122  1156  simp123  1157  simp131  1158  simp132  1159  simp133  1160  3anim123i  1210  3jaao  1344  ceqsalt  2829  sbciegft  3062  reupick2  3493  ifbothdc  3640  frirrg  4447  breldmg  4937  fntpg  5386  funimaexglem  5413  fex2  5503  fvun1  5712  fprg  5836  fsnunfv  5854  fnfvima  5888  cocan1  5927  cocan2  5928  mpoeq3dv  6086  fovcld  6125  fvmpopr2d  6157  funexw  6273  mpofvex  6369  poxp  6396  smoiso  6467  tfrlem5  6479  tfrlemibxssdm  6492  tfr1onlembfn  6509  tfri1dALT  6516  tfrcllembfn  6522  rdgon  6551  freccllem  6567  nnawordex  6696  1dom1el  6992  mapxpen  7033  fidceq  7055  fidifsnen  7056  dif1en  7067  en2eqpr  7098  unsnfi  7110  unsnfidcex  7111  unsnfidcel  7112  fisseneq  7126  ordiso2  7233  updjud  7280  mkvprop  7356  endjudisj  7424  xpdjuen  7432  mulcanenq0ec  7664  prltlu  7706  prarloclem3step  7715  prarloclem5  7719  ltasrg  7989  cnegexlem1  8353  addcan  8358  apcotr  8786  apadd1  8787  mulext1  8791  divdivap1  8902  divdivap2  8903  div2negap  8914  divneg2ap  8915  ltmulgt11  9043  ltdiv2  9066  squeeze0  9083  nndivtr  9184  nn0n0n1ge2  9549  zdivmul  9569  gtndiv  9574  eluzuzle  9763  eluzp1p1  9781  qdivcl  9876  irrmul  9880  rpgecl  9916  xaddass  10103  xltadd1  10110  xlt2add  10114  lbico1  10164  lbicc2  10218  zltaddlt1le  10241  uzsubsubfz  10281  elfz1b  10324  elfz0ubfz0  10359  fz0fzelfz0  10361  difelfzle  10368  difelfznle  10369  2ffzeq  10375  fzo1fzo0n0  10421  ubmelfzo  10444  fzonn0p1p1  10457  elfzom1p1elfzo  10458  elfzonelfzo  10474  subfzo0  10487  ceiqle  10574  ceilqle  10575  modqval  10585  flqpmodeq  10588  modq0  10590  negqmod0  10592  modqge0  10593  modqlt  10594  modqdiffl  10596  modqmulnn  10603  modqvalp1  10604  modqmuladdnn0  10629  qnegmod  10630  addmodid  10633  modfzo0difsn  10656  addmodlteq  10659  qexpclz  10821  expgt1  10838  expp1zap  10849  expm1ap  10850  expubnd  10857  bernneq2  10922  expnlbnd  10925  mulsubdivbinom2ap  10972  omgadd  11064  hashun  11067  fihashssdif  11081  hashdifpr  11083  fimaxq  11090  ccatval2  11174  ccatval3  11175  ccatval1lsw  11180  ccatval21sw  11181  ccatass  11184  ccatw2s1leng  11214  ccats1val2  11216  ccat2s1fvwd  11223  fzowrddc  11227  swrdval  11228  swrdclg  11230  swrdval2  11231  swrdnd  11239  swrdlen2  11242  swrdfv2  11243  ccatswrd  11250  pfxn0  11268  pfxsuff1eqwrdeq  11279  swrdswrdlem  11284  ccats1pfxeq  11294  ccats1pfxeqrex  11295  ccatopth2  11297  wrd2ind  11303  pfxccatin12lem3  11312  pfxccat3  11314  swrdccat  11315  pfxccatpfx2  11317  pfxccat3a  11318  swrdccat3b  11320  pfxccatid  11321  ccats1pfxeqbi  11322  shftuz  11377  mulreap  11424  redivap  11434  imdivap  11441  resqrtcl  11589  xrmaxltsup  11818  xrmaxaddlem  11820  xrmaxadd  11821  xrlemininf  11831  xrminltinf  11832  climuni  11853  addcn2  11870  mulcn2  11872  efsub  12241  sin02gt0  12324  cos12dec  12328  dvdsval2  12350  addmodlteqALT  12419  modremain  12489  fldivndvdslt  12497  mulgcdr  12588  gcddiv  12589  rpmulgcd  12596  rplpwr  12597  rppwr  12598  nnminle  12605  qredeq  12667  divgcdcoprmex  12673  cncongr1  12674  cncongr2  12675  dvdsnprmd  12696  euclemma  12717  prmexpb  12722  qnumdenbi  12763  eulerth  12804  fermltl  12805  prmdiv  12806  hashgcdlem  12809  odzcllem  12814  vfermltl  12823  reumodprminv  12825  modprm0  12826  modprmn0modprm0  12828  coprimeprodsq  12829  pythagtriplem1  12837  pythagtriplem3  12839  pythagtriplem4  12840  pythagtriplem10  12841  pythagtriplem6  12842  pythagtriplem7  12843  pythagtriplem8  12844  pythagtriplem9  12845  pythagtriplem11  12846  pythagtriplem12  12847  pythagtriplem13  12848  pythagtriplem14  12849  pythagtriplem15  12850  pythagtriplem16  12851  pythagtriplem17  12852  pythagtriplem19  12854  pythagtrip  12855  pcpremul  12865  pcdvdsb  12892  dvdsprmpweqnn  12908  dvdsprmpweqle  12909  difsqpwdvds  12910  pcfaclem  12921  pcbc  12923  4sqlem12  12974  unennn  13017  nninfdc  13073  setsex  13113  f1ocpbllem  13392  imasaddfnlemg  13396  imasaddvallemg  13397  ercpbl  13413  erlecpbl  13414  qusaddvallemg  13415  fvprif  13425  xpsfrnel2  13428  plusfvalg  13445  imasmnd  13535  insubm  13567  grpidrcan  13647  grpidlcan  13648  grpsubpropd2  13687  pwsinvg  13694  imasgrp2  13696  imasgrp  13697  mulgnnsubcl  13720  mulgnn0subcl  13721  mulgsubcl  13722  mulgaddcom  13732  mulginvcom  13733  mulgnnass  13743  mulgassr  13746  mulgpropdg  13750  submmulg  13752  subgcl  13770  subgsubcl  13771  subgsub  13772  subgmulg  13774  nsgconj  13792  ghmsub  13837  ghmrn  13843  ghmeqker  13857  f1ghm0to0  13858  ablinvadd  13896  ablsub4  13899  abladdsub4  13900  subcmnd  13919  imasabl  13922  rngcl  13956  imasrng  13968  srgcl  13982  srg1zr  13999  srgen1zr  14000  ringcl  14025  crngcom  14026  ringidss  14041  mulgass2  14070  imasring  14076  opprmulg  14083  unitmulclb  14127  unitdvcl  14149  rhmmul  14177  rhmdvdsr  14188  subrngmcl  14222  subrgmcl  14246  subrgdv  14251  subrgugrp  14253  domneq0  14285  scafvalg  14320  lmodprop2d  14361  lssclg  14377  lssvnegcl  14389  lssintclm  14397  sralmod  14463  rnglidlmcl  14493  lidlnegcl  14498  rspssp  14507  rnglidlmsgrp  14510  rnglidlrng  14511  2idlcpblrng  14536  qus2idrng  14538  zndvds  14662  znleval2  14667  basgen  14803  2basgeng  14805  iuncld  14838  neipsm  14877  opnneissb  14878  opnssneib  14879  iscnp3  14926  cnprcl2k  14929  cnpnei  14942  cncnp2m  14954  cnptoprest  14962  sslm  14970  upxp  14995  cnmpt22  15017  distspace  15058  0met  15107  blvalps  15111  blval  15112  ssblps  15148  ssbl  15149  blpnfctr  15162  blopn  15213  blnei  15215  bdxmet  15224  bdbl  15226  metcnp3  15234  tgqioo  15278  ptolemy  15547  sinq12gt0  15553  sincosq1eq  15562  rpcxpadd  15628  cxpmul  15635  rplogbval  15668  logbleb  15684  logbgcd1irr  15690  logbprmirr  15695  lgsfvalg  15733  lgsneg1  15753  lgssq  15768  lgsdinn0  15776  gausslemma2dlem1a  15786  2lgs  15832  2lgsoddprmlem2  15834  funvtxdm2domval  15879  funiedgdm2domval  15880  iedgedgg  15911  lpvtx  15929  incistruhgr  15940  ausgrumgrien  16020  ausgrusgrien  16021  umgr2edgneu  16062  ushgredgedg  16076  ushgredgedgloop  16078  usgr2v1e2w  16096  egrsubgr  16113  subumgredg2en  16121  iswlk  16173  wlkl1loop  16208  uspgr2wlkeq  16215  istrl  16235  clwwlkccatlem  16250  clwwlkccat  16251  clwwlknccat  16273  clwwlknonex2lem2  16288  clwwlknonex2  16289  iseupth  16297  bdfind  16541