Theorem 3ad2ant3 1051

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 1046	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:  simp3l  1056  simp3r  1057  simp31  1064  simp32  1065  simp33  1066  simp3ll  1099  simp3lr  1100  simp3rl  1101  simp3rr  1102  simp3l1  1133  simp3l2  1134  simp3l3  1135  simp3r1  1136  simp3r2  1137  simp3r3  1138  simp31l  1151  simp31r  1152  simp32l  1153  simp32r  1154  simp33l  1155  simp33r  1156  simp311  1175  simp312  1176  simp313  1177  simp321  1178  simp322  1179  simp323  1180  simp331  1181  simp332  1182  simp333  1183  3anim123i  1215  3jaao  1349  ceqsalt  2848  ceqsralt  2849  vtoclgft  2873  ifbothdc  3675  ifnebibdc  3686  ssprsseq  3877  tpssi  3884  sotricim  4468  elirr  4688  en2lp  4701  reg3exmidlemwe  4726  sotri2  5185  poltletr  5188  funprg  5431  funtpg  5432  fntpg  5437  funimaexglem  5464  fvun1  5769  ftpg  5899  fsnunf  5915  fsnunfv  5916  caovimo  6283  funsssuppss  6498  brtposg  6525  smoel  6571  rdgivallem  6652  frecsuclem  6677  domssr  7064  mapxpen  7148  unsnfi  7226  unsnfidcex  7227  unsnfidcel  7228  sbthlemi4  7277  elfir  7307  updjud  7422  ltsopi  7687  distrnqg  7754  ltmnqg  7768  mulcanenq0ec  7812  distrnq0  7826  prarloclem5  7867  1idprl  7957  1idpru  7958  ltaprg  7986  recexprlemopl  7992  recexprlemopu  7994  recexprlem1ssl  8000  aptipr  8008  ltmprr  8009  cauappcvgprlemlol  8014  cauappcvgprlemupu  8016  caucvgprlemlol  8037  caucvgprlemupu  8039  caucvgprprlemlol  8065  caucvgprprlemupu  8067  readdcan  8466  cnegexlem2  8502  addcan2  8507  ltadd2  8747  apreap  8915  ltmul1  8920  apcotr  8935  apadd1  8936  mulext1  8940  divdirap  9027  divcanap5  9044  ltdiv1  9198  ind1  9300  ind0  9301  lt2halves  9541  zdivmul  9736  eluzsub  9952  ledivge1le  10127  addlelt  10169  xaddass  10271  xleadd1  10277  xltadd1  10278  elioo5  10335  iccsupr  10368  iccneg  10391  icoshft  10392  icoshftf1o  10393  zltaddlt1le  10410  fzen  10447  elfz1b  10497  fzrevral  10512  fzshftral  10515  elfz0ubfz0  10532  elfz0fzfz0  10533  fz0fzelfz0  10534  fz0fzdiffz0  10537  elfzo  10556  fzodcel  10560  elfzonlteqm1  10628  modqaddmulmod  10828  expdivap  11027  leexp2a  11029  bcval3  11189  omgadd  11242  ccatval1  11365  ccatval2  11366  ccatval3  11367  ccatass  11376  ccats1val2  11408  swrdval2  11423  swrdlen  11424  pfxfv  11456  pfxnd  11461  pfxsuffeqwrdeq  11470  swrdswrdlem  11476  swrdswrd  11477  pfxswrd  11478  pfxpfx  11480  ccats1pfxeq  11486  ccats1pfxeqrex  11487  pfxccatin12lem2  11503  pfxccatpfx1  11508  swrdccat3b  11512  pfxccatid  11513  shftfibg  11585  elicc4abs  11860  xrmaxltsup  12024  xrmaxadd  12027  xrlemininf  12037  xrminltinf  12038  mulcn2  12078  fsumsplitsnun  12186  prodfrecap  12313  demoivreALT  12541  dvdsval2  12557  dvdsmodexp  12562  dvdsmulcr  12588  modmulconst  12590  dvdsexp  12628  oddge22np1  12648  modremain  12696  mulgcd  12793  mulgcdr  12795  gcddiv  12796  rpmulgcd  12803  rplpwr  12804  coprmdvds  12870  cncongr1  12881  dvdsnprmd  12903  prmexpb  12929  rpexp  12931  cncongrprm  12935  modprm0  13033  modprmn0modprm0  13035  coprimeprodsq  13036  pythagtriplem1  13044  pythagtriplem3  13046  pythagtriplem10  13048  pythagtriplem6  13049  pythagtriplem11  13053  pythagtriplem12  13054  pythagtriplem13  13055  pythagtriplem15  13057  pythagtriplem17  13059  pythagtriplem19  13061  pcdvdsb  13099  dvdsprmpweqle  13116  pcfaclem  13128  ballotfilemieq  13260  ballotfilemrv1  13264  isstructr  13367  setsvala  13383  setsresg  13390  strle3g  13462  imasaddvallemg  13636  fvprif  13664  mgmsscl  13681  insubm  13792  dfgrp3mlem  13903  mulgdirlem  13956  mulgp1  13958  mulgmodid  13964  eqglact  14028  gsumconstcmn  14166  rngdi  14239  rngdir  14240  rmodislmodlem  14687  rmodislmod  14688  lssclg  14701  2idlcpblrng  14860  qusmulrng  14869  assa2ass  15009  assa2ass2  15010  psrbagaddclfi  15061  clsss  15219  ntrcls0  15232  neiss  15251  neipsm  15255  cnpnei  15320  cncnp2m  15332  cnconst2  15334  sslm  15348  upxp  15373  txmetcn  15620  ptolemy  15925  sincosq1eq  15940  rplogbval  16047  rpcxplogb  16066  pellexlem1  16091  lgsdirprm  16153  lgsdirnn0  16166  gausslemma2dlem1a  16177  gausslemma2dlem3  16182  2lgslem1a1  16205  2lgsoddprmlem1  16224  2lgsoddprmlem2  16225  structiedg0val  16281  lpvtx  16320  incistruhgr  16331  upgredg2vtx  16389  upgredgpr  16390  ausgrumgrien  16411  ausgrusgrien  16412  ushgredgedg  16467  ushgredgedgloop  16469  uhgrissubgr  16502  egrsubgr  16504  0uhgrsubgr  16506  wlkvtxeledgg  16585  wlkeq  16595  wlkl1loop  16599  uspgr2wlkeq  16606  uspgr2wlkeq2  16607  wlkres  16620  loopclwwlkn1b  16660  clwwlkext2edg  16663  clwwlknonex2lem2  16679  clwwlknonex2  16680  clwwlknun  16682  eupth2lem3lem6fi  16712  findset  16971