Theorem 3ad2ant3 1047

Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)

Hypothesis

Ref	Expression
3ad2ant.1	⊢ (𝜑 → 𝜒)

Assertion

Ref	Expression
3ad2ant3	⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒)

Proof of Theorem 3ad2ant3

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	adantl 277	. 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜒)
3	2	3adant1 1042	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:  simp3l  1052  simp3r  1053  simp31  1060  simp32  1061  simp33  1062  simp3ll  1095  simp3lr  1096  simp3rl  1097  simp3rr  1098  simp3l1  1129  simp3l2  1130  simp3l3  1131  simp3r1  1132  simp3r2  1133  simp3r3  1134  simp31l  1147  simp31r  1148  simp32l  1149  simp32r  1150  simp33l  1151  simp33r  1152  simp311  1171  simp312  1172  simp313  1173  simp321  1174  simp322  1175  simp323  1176  simp331  1177  simp332  1178  simp333  1179  3anim123i  1211  3jaao  1345  ceqsalt  2842  ceqsralt  2843  vtoclgft  2867  ifbothdc  3661  ifnebibdc  3672  ssprsseq  3861  tpssi  3868  sotricim  4449  elirr  4668  en2lp  4681  reg3exmidlemwe  4706  sotri2  5165  poltletr  5168  funprg  5411  funtpg  5412  fntpg  5417  funimaexglem  5444  fvun1  5748  ftpg  5873  fsnunf  5889  fsnunfv  5890  caovimo  6256  funsssuppss  6471  brtposg  6498  smoel  6544  rdgivallem  6625  frecsuclem  6650  domssr  7030  mapxpen  7114  unsnfi  7192  unsnfidcex  7193  unsnfidcel  7194  sbthlemi4  7243  elfir  7273  updjud  7386  ltsopi  7651  distrnqg  7718  ltmnqg  7732  mulcanenq0ec  7776  distrnq0  7790  prarloclem5  7831  1idprl  7921  1idpru  7922  ltaprg  7950  recexprlemopl  7956  recexprlemopu  7958  recexprlem1ssl  7964  aptipr  7972  ltmprr  7973  cauappcvgprlemlol  7978  cauappcvgprlemupu  7980  caucvgprlemlol  8001  caucvgprlemupu  8003  caucvgprprlemlol  8029  caucvgprprlemupu  8031  readdcan  8429  cnegexlem2  8465  addcan2  8470  ltadd2  8710  apreap  8878  ltmul1  8883  apcotr  8898  apadd1  8899  mulext1  8903  divdirap  8988  divcanap5  9005  ltdiv1  9159  lt2halves  9491  zdivmul  9686  eluzsub  9902  ledivge1le  10077  addlelt  10119  xaddass  10221  xleadd1  10227  xltadd1  10228  elioo5  10285  iccsupr  10318  iccneg  10341  icoshft  10342  icoshftf1o  10343  zltaddlt1le  10360  fzen  10397  elfz1b  10446  fzrevral  10461  fzshftral  10464  elfz0ubfz0  10481  elfz0fzfz0  10482  fz0fzelfz0  10483  fz0fzdiffz0  10486  elfzo  10505  fzodcel  10509  elfzonlteqm1  10577  modqaddmulmod  10777  expdivap  10976  leexp2a  10978  bcval3  11138  omgadd  11191  ccatval1  11310  ccatval2  11311  ccatval3  11312  ccatass  11321  ccats1val2  11353  swrdval2  11368  swrdlen  11369  pfxfv  11401  pfxnd  11406  pfxsuffeqwrdeq  11415  swrdswrdlem  11421  swrdswrd  11422  pfxswrd  11423  pfxpfx  11425  ccats1pfxeq  11431  ccats1pfxeqrex  11432  pfxccatin12lem2  11448  pfxccatpfx1  11453  swrdccat3b  11457  pfxccatid  11458  shftfibg  11530  elicc4abs  11804  xrmaxltsup  11968  xrmaxadd  11971  xrlemininf  11981  xrminltinf  11982  mulcn2  12022  fsumsplitsnun  12130  prodfrecap  12257  demoivreALT  12485  dvdsval2  12501  dvdsmodexp  12506  dvdsmulcr  12532  modmulconst  12534  dvdsexp  12572  oddge22np1  12592  modremain  12640  mulgcd  12737  mulgcdr  12739  gcddiv  12740  rpmulgcd  12747  rplpwr  12748  coprmdvds  12814  cncongr1  12825  dvdsnprmd  12847  prmexpb  12873  rpexp  12875  cncongrprm  12879  modprm0  12977  modprmn0modprm0  12979  coprimeprodsq  12980  pythagtriplem1  12988  pythagtriplem3  12990  pythagtriplem10  12992  pythagtriplem6  12993  pythagtriplem11  12997  pythagtriplem12  12998  pythagtriplem13  12999  pythagtriplem15  13001  pythagtriplem17  13003  pythagtriplem19  13005  pcdvdsb  13043  dvdsprmpweqle  13060  pcfaclem  13072  ballotfilemieq  13204  ballotfilemrv1  13208  isstructr  13311  setsvala  13327  setsresg  13334  strle3g  13405  imasaddvallemg  13579  fvprif  13607  mgmsscl  13624  insubm  13740  dfgrp3mlem  13853  mulgdirlem  13906  mulgp1  13908  mulgmodid  13914  eqglact  13978  rngdi  14179  rngdir  14180  rmodislmodlem  14624  rmodislmod  14625  lssclg  14638  2idlcpblrng  14797  qusmulrng  14806  psrbagaddclfi  14951  clsss  15109  ntrcls0  15122  neiss  15141  neipsm  15145  cnpnei  15210  cncnp2m  15222  cnconst2  15224  sslm  15238  upxp  15263  txmetcn  15510  ptolemy  15815  sincosq1eq  15830  rplogbval  15936  rpcxplogb  15955  pellexlem1  15971  lgsdirprm  16033  lgsdirnn0  16046  gausslemma2dlem1a  16057  gausslemma2dlem3  16062  2lgslem1a1  16085  2lgsoddprmlem1  16104  2lgsoddprmlem2  16105  structiedg0val  16161  lpvtx  16200  incistruhgr  16211  upgredg2vtx  16269  upgredgpr  16270  ausgrumgrien  16291  ausgrusgrien  16292  ushgredgedg  16347  ushgredgedgloop  16349  uhgrissubgr  16382  egrsubgr  16384  0uhgrsubgr  16386  wlkvtxeledgg  16465  wlkeq  16475  wlkl1loop  16479  uspgr2wlkeq  16486  uspgr2wlkeq2  16487  wlkres  16500  loopclwwlkn1b  16540  clwwlkext2edg  16543  clwwlknonex2lem2  16559  clwwlknonex2  16560  clwwlknun  16562  eupth2lem3lem6fi  16592  findset  16841