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  2830  ceqsralt  2831  vtoclgft  2855  ifbothdc  3644  ifnebibdc  3655  ssprsseq  3840  tpssi  3847  sotricim  4426  elirr  4645  en2lp  4658  reg3exmidlemwe  4683  sotri2  5141  poltletr  5144  funprg  5387  funtpg  5388  fntpg  5393  funimaexglem  5420  fvun1  5721  ftpg  5846  fsnunf  5862  fsnunfv  5863  caovimo  6226  funsssuppss  6436  brtposg  6463  smoel  6509  rdgivallem  6590  frecsuclem  6615  domssr  6994  mapxpen  7077  unsnfi  7154  unsnfidcex  7155  unsnfidcel  7156  sbthlemi4  7202  elfir  7215  updjud  7324  ltsopi  7583  distrnqg  7650  ltmnqg  7664  mulcanenq0ec  7708  distrnq0  7722  prarloclem5  7763  1idprl  7853  1idpru  7854  ltaprg  7882  recexprlemopl  7888  recexprlemopu  7890  recexprlem1ssl  7896  aptipr  7904  ltmprr  7905  cauappcvgprlemlol  7910  cauappcvgprlemupu  7912  caucvgprlemlol  7933  caucvgprlemupu  7935  caucvgprprlemlol  7961  caucvgprprlemupu  7963  readdcan  8361  cnegexlem2  8397  addcan2  8402  ltadd2  8641  apreap  8809  ltmul1  8814  apcotr  8829  apadd1  8830  mulext1  8834  divdirap  8919  divcanap5  8936  ltdiv1  9090  lt2halves  9422  zdivmul  9614  eluzsub  9830  ledivge1le  10005  addlelt  10047  xaddass  10148  xleadd1  10154  xltadd1  10155  elioo5  10212  iccsupr  10245  iccneg  10268  icoshft  10269  icoshftf1o  10270  zltaddlt1le  10287  fzen  10323  elfz1b  10370  fzrevral  10385  fzshftral  10388  elfz0ubfz0  10405  elfz0fzfz0  10406  fz0fzelfz0  10407  fz0fzdiffz0  10410  elfzo  10429  fzodcel  10433  elfzonlteqm1  10501  modqaddmulmod  10699  expdivap  10898  leexp2a  10900  bcval3  11059  omgadd  11111  ccatval1  11223  ccatval2  11224  ccatval3  11225  ccatass  11234  ccats1val2  11266  swrdval2  11281  swrdlen  11282  pfxfv  11314  pfxnd  11319  pfxsuffeqwrdeq  11328  swrdswrdlem  11334  swrdswrd  11335  pfxswrd  11336  pfxpfx  11338  ccats1pfxeq  11344  ccats1pfxeqrex  11345  pfxccatin12lem2  11361  pfxccatpfx1  11366  swrdccat3b  11370  pfxccatid  11371  shftfibg  11443  elicc4abs  11717  xrmaxltsup  11881  xrmaxadd  11884  xrlemininf  11894  xrminltinf  11895  mulcn2  11935  fsumsplitsnun  12043  prodfrecap  12170  demoivreALT  12398  dvdsval2  12414  dvdsmodexp  12419  dvdsmulcr  12445  modmulconst  12447  dvdsexp  12485  oddge22np1  12505  modremain  12553  mulgcd  12650  mulgcdr  12652  gcddiv  12653  rpmulgcd  12660  rplpwr  12661  coprmdvds  12727  cncongr1  12738  dvdsnprmd  12760  prmexpb  12786  rpexp  12788  cncongrprm  12792  modprm0  12890  modprmn0modprm0  12892  coprimeprodsq  12893  pythagtriplem1  12901  pythagtriplem3  12903  pythagtriplem10  12905  pythagtriplem6  12906  pythagtriplem11  12910  pythagtriplem12  12911  pythagtriplem13  12912  pythagtriplem15  12914  pythagtriplem17  12916  pythagtriplem19  12918  pcdvdsb  12956  dvdsprmpweqle  12973  pcfaclem  12985  isstructr  13160  setsvala  13176  setsresg  13183  strle3g  13254  imasaddvallemg  13461  fvprif  13489  mgmsscl  13507  insubm  13631  dfgrp3mlem  13744  mulgdirlem  13803  mulgp1  13805  mulgmodid  13811  eqglact  13875  rngdi  14017  rngdir  14018  rmodislmodlem  14429  rmodislmod  14430  lssclg  14443  2idlcpblrng  14602  qusmulrng  14611  clsss  14912  ntrcls0  14925  neiss  14944  neipsm  14948  cnpnei  15013  cncnp2m  15025  cnconst2  15027  sslm  15041  upxp  15066  txmetcn  15313  ptolemy  15618  sincosq1eq  15633  rplogbval  15739  rpcxplogb  15758  pellexlem1  15774  lgsdirprm  15836  lgsdirnn0  15849  gausslemma2dlem1a  15860  gausslemma2dlem3  15865  2lgslem1a1  15888  2lgsoddprmlem1  15907  2lgsoddprmlem2  15908  structiedg0val  15964  lpvtx  16003  incistruhgr  16014  upgredg2vtx  16072  upgredgpr  16073  ausgrumgrien  16094  ausgrusgrien  16095  ushgredgedg  16150  ushgredgedgloop  16152  uhgrissubgr  16185  egrsubgr  16187  0uhgrsubgr  16189  wlkvtxeledgg  16268  wlkeq  16278  wlkl1loop  16282  uspgr2wlkeq  16289  uspgr2wlkeq2  16290  wlkres  16303  loopclwwlkn1b  16343  clwwlkext2edg  16346  clwwlknonex2lem2  16362  clwwlknonex2  16363  clwwlknun  16365  eupth2lem3lem6fi  16395  findset  16644