Theorem 3ad2ant3 1046

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 1041	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:  simp3l  1051  simp3r  1052  simp31  1059  simp32  1060  simp33  1061  simp3ll  1094  simp3lr  1095  simp3rl  1096  simp3rr  1097  simp3l1  1128  simp3l2  1129  simp3l3  1130  simp3r1  1131  simp3r2  1132  simp3r3  1133  simp31l  1146  simp31r  1147  simp32l  1148  simp32r  1149  simp33l  1150  simp33r  1151  simp311  1170  simp312  1171  simp313  1172  simp321  1173  simp322  1174  simp323  1175  simp331  1176  simp332  1177  simp333  1178  3anim123i  1210  3jaao  1344  ceqsalt  2829  ceqsralt  2830  vtoclgft  2854  ifbothdc  3640  ifnebibdc  3651  ssprsseq  3835  tpssi  3842  sotricim  4420  elirr  4639  en2lp  4652  reg3exmidlemwe  4677  sotri2  5134  poltletr  5137  funprg  5380  funtpg  5381  fntpg  5386  funimaexglem  5413  fvun1  5712  ftpg  5837  fsnunf  5853  fsnunfv  5854  caovimo  6215  brtposg  6419  smoel  6465  rdgivallem  6546  frecsuclem  6571  domssr  6950  mapxpen  7033  unsnfi  7110  unsnfidcex  7111  unsnfidcel  7112  sbthlemi4  7158  elfir  7171  updjud  7280  ltsopi  7539  distrnqg  7606  ltmnqg  7620  mulcanenq0ec  7664  distrnq0  7678  prarloclem5  7719  1idprl  7809  1idpru  7810  ltaprg  7838  recexprlemopl  7844  recexprlemopu  7846  recexprlem1ssl  7852  aptipr  7860  ltmprr  7861  cauappcvgprlemlol  7866  cauappcvgprlemupu  7868  caucvgprlemlol  7889  caucvgprlemupu  7891  caucvgprprlemlol  7917  caucvgprprlemupu  7919  readdcan  8318  cnegexlem2  8354  addcan2  8359  ltadd2  8598  apreap  8766  ltmul1  8771  apcotr  8786  apadd1  8787  mulext1  8791  divdirap  8876  divcanap5  8893  ltdiv1  9047  lt2halves  9379  zdivmul  9569  eluzsub  9785  ledivge1le  9960  addlelt  10002  xaddass  10103  xleadd1  10109  xltadd1  10110  elioo5  10167  iccsupr  10200  iccneg  10223  icoshft  10224  icoshftf1o  10225  zltaddlt1le  10241  fzen  10277  elfz1b  10324  fzrevral  10339  fzshftral  10342  elfz0ubfz0  10359  elfz0fzfz0  10360  fz0fzelfz0  10361  fz0fzdiffz0  10364  elfzo  10383  fzodcel  10387  elfzonlteqm1  10454  modqaddmulmod  10652  expdivap  10851  leexp2a  10853  bcval3  11012  omgadd  11064  ccatval1  11173  ccatval2  11174  ccatval3  11175  ccatass  11184  ccats1val2  11216  swrdval2  11231  swrdlen  11232  pfxfv  11264  pfxnd  11269  pfxsuffeqwrdeq  11278  swrdswrdlem  11284  swrdswrd  11285  pfxswrd  11286  pfxpfx  11288  ccats1pfxeq  11294  ccats1pfxeqrex  11295  pfxccatin12lem2  11311  pfxccatpfx1  11316  swrdccat3b  11320  pfxccatid  11321  shftfibg  11380  elicc4abs  11654  xrmaxltsup  11818  xrmaxadd  11821  xrlemininf  11831  xrminltinf  11832  mulcn2  11872  fsumsplitsnun  11979  prodfrecap  12106  demoivreALT  12334  dvdsval2  12350  dvdsmodexp  12355  dvdsmulcr  12381  modmulconst  12383  dvdsexp  12421  oddge22np1  12441  modremain  12489  mulgcd  12586  mulgcdr  12588  gcddiv  12589  rpmulgcd  12596  rplpwr  12597  coprmdvds  12663  cncongr1  12674  dvdsnprmd  12696  prmexpb  12722  rpexp  12724  cncongrprm  12728  modprm0  12826  modprmn0modprm0  12828  coprimeprodsq  12829  pythagtriplem1  12837  pythagtriplem3  12839  pythagtriplem10  12841  pythagtriplem6  12842  pythagtriplem11  12846  pythagtriplem12  12847  pythagtriplem13  12848  pythagtriplem15  12850  pythagtriplem17  12852  pythagtriplem19  12854  pcdvdsb  12892  dvdsprmpweqle  12909  pcfaclem  12921  isstructr  13096  setsvala  13112  setsresg  13119  strle3g  13190  imasaddvallemg  13397  fvprif  13425  mgmsscl  13443  insubm  13567  dfgrp3mlem  13680  mulgdirlem  13739  mulgp1  13741  mulgmodid  13747  eqglact  13811  rngdi  13952  rngdir  13953  rmodislmodlem  14363  rmodislmod  14364  lssclg  14377  2idlcpblrng  14536  qusmulrng  14545  clsss  14841  ntrcls0  14854  neiss  14873  neipsm  14877  cnpnei  14942  cncnp2m  14954  cnconst2  14956  sslm  14970  upxp  14995  txmetcn  15242  ptolemy  15547  sincosq1eq  15562  rplogbval  15668  rpcxplogb  15687  lgsdirprm  15762  lgsdirnn0  15775  gausslemma2dlem1a  15786  gausslemma2dlem3  15791  2lgslem1a1  15814  2lgsoddprmlem1  15833  2lgsoddprmlem2  15834  structiedg0val  15890  lpvtx  15929  incistruhgr  15940  upgredg2vtx  15998  upgredgpr  15999  ausgrumgrien  16020  ausgrusgrien  16021  ushgredgedg  16076  ushgredgedgloop  16078  uhgrissubgr  16111  egrsubgr  16113  0uhgrsubgr  16115  wlkvtxeledgg  16194  wlkeq  16204  wlkl1loop  16208  uspgr2wlkeq  16215  uspgr2wlkeq2  16216  wlkres  16229  loopclwwlkn1b  16269  clwwlkext2edg  16272  clwwlknonex2lem2  16288  clwwlknonex2  16289  clwwlknun  16291  findset  16540