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  4470  elirr  4690  en2lp  4703  reg3exmidlemwe  4728  sotri2  5188  poltletr  5191  funprg  5434  funtpg  5435  fntpg  5440  funimaexglem  5467  fvun1  5772  ftpg  5902  fsnunf  5918  fsnunfv  5919  caovimo  6286  funsssuppss  6502  brtposg  6530  smoel  6576  rdgivallem  6657  frecsuclem  6682  mapm  6975  domssr  7070  mapxpen  7154  unsnfi  7232  unsnfidcex  7233  unsnfidcel  7234  sbthlemi4  7284  elfir  7312  updjud  7428  ltsopi  7693  distrnqg  7760  ltmnqg  7774  mulcanenq0ec  7818  distrnq0  7832  prarloclem5  7873  1idprl  7963  1idpru  7964  ltaprg  7992  recexprlemopl  7998  recexprlemopu  8000  recexprlem1ssl  8006  aptipr  8014  ltmprr  8015  cauappcvgprlemlol  8020  cauappcvgprlemupu  8022  caucvgprlemlol  8043  caucvgprlemupu  8045  caucvgprprlemlol  8071  caucvgprprlemupu  8073  readdcan  8473  cnegexlem2  8509  addcan2  8514  ltadd2  8754  apreap  8923  ltmul1  8928  apcotr  8943  apadd1  8944  mulext1  8948  divdirap  9035  divcanap5  9052  ltdiv1  9206  ind1  9309  ind0  9310  lt2halves  9552  zdivmul  9746  eluzsub  9967  ledivge1le  10143  addlelt  10185  xaddass  10287  xleadd1  10293  xltadd1  10294  elioo5  10351  iccsupr  10384  iccneg  10407  icoshft  10408  icoshftf1o  10409  zltaddlt1le  10426  fzen  10463  elfz1b  10513  fzrevral  10528  fzshftral  10531  elfz0ubfz0  10548  elfz0fzfz0  10549  fz0fzelfz0  10550  fz0fzdiffz0  10553  elfzo  10572  fzodcel  10576  elfzonlteqm1  10644  modqaddmulmod  10848  expdivap  11047  leexp2a  11049  bcval3  11210  omgadd  11263  ccatval1  11386  ccatval2  11387  ccatval3  11388  ccatass  11397  ccats1val2  11429  swrdval2  11444  swrdlen  11445  pfxfv  11477  pfxnd  11482  pfxsuffeqwrdeq  11491  swrdswrdlem  11497  swrdswrd  11498  pfxswrd  11499  pfxpfx  11501  ccats1pfxeq  11507  ccats1pfxeqrex  11508  pfxccatin12lem2  11524  pfxccatpfx1  11529  swrdccat3b  11533  pfxccatid  11534  shftfibg  11606  elicc4abs  11882  xrmaxltsup  12048  xrmaxadd  12051  xrlemininf  12061  xrminltinf  12062  mulcn2  12102  fsumsplitsnun  12210  prodfrecap  12337  demoivreALT  12565  dvdsval2  12581  dvdsmodexp  12586  dvdsmulcr  12612  modmulconst  12614  dvdsexp  12652  oddge22np1  12672  modremain  12720  mulgcd  12817  mulgcdr  12819  gcddiv  12820  rpmulgcd  12827  rplpwr  12828  coprmdvds  12894  cncongr1  12905  dvdsnprmd  12927  prmexpb  12954  rpexp  12956  cncongrprm  12960  modprm0  13061  modprmn0modprm0  13063  coprimeprodsq  13064  pythagtriplem1  13072  pythagtriplem3  13074  pythagtriplem10  13076  pythagtriplem6  13077  pythagtriplem11  13081  pythagtriplem12  13082  pythagtriplem13  13083  pythagtriplem15  13085  pythagtriplem17  13087  pythagtriplem19  13089  pcdvdsb  13127  dvdsprmpweqle  13144  pcfaclem  13156  ballotfilemieq  13317  ballotfilemrv1  13321  isstructr  13424  setsvala  13440  setsresg  13447  strle3g  13520  imasaddvallemg  13694  fvprif  13722  mgmsscl  13739  insubm  13850  dfgrp3mlem  13961  mulgdirlem  14014  mulgp1  14016  mulgmodid  14022  eqglact  14086  gsumconstcmn  14265  rngdi  14345  rngdir  14346  rmodislmodlem  14795  rmodislmod  14796  lssclg  14809  2idlcpblrng  14968  qusmulrng  14977  assa2ass  15117  assa2ass2  15118  psrbagaddclfi  15173  clsss  15361  ntrcls0  15374  neiss  15393  neipsm  15397  cnpnei  15462  cncnp2m  15474  cnconst2  15476  sslm  15490  upxp  15515  txmetcn  15762  ptolemy  16068  sincosq1eq  16083  rplogbval  16198  rpcxplogb  16217  pellexlem1  16246  bcmono  16321  lgsdirprm  16375  lgsdirnn0  16388  gausslemma2dlem1a  16399  gausslemma2dlem3  16404  2lgslem1a1  16427  2lgsoddprmlem1  16446  2lgsoddprmlem2  16447  structiedg0val  16503  lpvtx  16542  incistruhgr  16553  upgredg2vtx  16611  upgredgpr  16612  ausgrumgrien  16633  ausgrusgrien  16634  ushgredgedg  16689  ushgredgedgloop  16691  uhgrissubgr  16724  egrsubgr  16726  0uhgrsubgr  16728  wlkvtxeledgg  16807  wlkeq  16817  wlkl1loop  16821  uspgr2wlkeq  16828  uspgr2wlkeq2  16829  wlkres  16842  loopclwwlkn1b  16882  clwwlkext2edg  16885  clwwlknonex2lem2  16901  clwwlknonex2  16902  clwwlknun  16904  eupth2lem3lem6fi  16934  findset  17193