Theorem 3ad2ant3 1023

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 1018	1 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  simp3l  1028  simp3r  1029  simp31  1036  simp32  1037  simp33  1038  simp3ll  1071  simp3lr  1072  simp3rl  1073  simp3rr  1074  simp3l1  1105  simp3l2  1106  simp3l3  1107  simp3r1  1108  simp3r2  1109  simp3r3  1110  simp31l  1123  simp31r  1124  simp32l  1125  simp32r  1126  simp33l  1127  simp33r  1128  simp311  1147  simp312  1148  simp313  1149  simp321  1150  simp322  1151  simp323  1152  simp331  1153  simp332  1154  simp333  1155  3anim123i  1187  3jaao  1321  ceqsalt  2800  ceqsralt  2801  vtoclgft  2825  ifbothdc  3610  ifnebibdc  3620  ssprsseq  3801  tpssi  3808  sotricim  4383  elirr  4602  en2lp  4615  reg3exmidlemwe  4640  sotri2  5094  poltletr  5097  funprg  5338  funtpg  5339  fntpg  5344  funimaexglem  5371  fvun1  5663  ftpg  5786  fsnunf  5802  fsnunfv  5803  caovimo  6158  brtposg  6358  smoel  6404  rdgivallem  6485  frecsuclem  6510  domssr  6887  mapxpen  6965  unsnfi  7037  unsnfidcex  7038  unsnfidcel  7039  sbthlemi4  7083  elfir  7096  updjud  7205  ltsopi  7463  distrnqg  7530  ltmnqg  7544  mulcanenq0ec  7588  distrnq0  7602  prarloclem5  7643  1idprl  7733  1idpru  7734  ltaprg  7762  recexprlemopl  7768  recexprlemopu  7770  recexprlem1ssl  7776  aptipr  7784  ltmprr  7785  cauappcvgprlemlol  7790  cauappcvgprlemupu  7792  caucvgprlemlol  7813  caucvgprlemupu  7815  caucvgprprlemlol  7841  caucvgprprlemupu  7843  readdcan  8242  cnegexlem2  8278  addcan2  8283  ltadd2  8522  apreap  8690  ltmul1  8695  apcotr  8710  apadd1  8711  mulext1  8715  divdirap  8800  divcanap5  8817  ltdiv1  8971  lt2halves  9303  zdivmul  9493  eluzsub  9708  ledivge1le  9878  addlelt  9920  xaddass  10021  xleadd1  10027  xltadd1  10028  elioo5  10085  iccsupr  10118  iccneg  10141  icoshft  10142  icoshftf1o  10143  zltaddlt1le  10159  fzen  10195  elfz1b  10242  fzrevral  10257  fzshftral  10260  elfz0ubfz0  10277  elfz0fzfz0  10278  fz0fzelfz0  10279  fz0fzdiffz0  10282  elfzo  10301  fzodcel  10305  elfzonlteqm1  10371  modqaddmulmod  10568  expdivap  10767  leexp2a  10769  bcval3  10928  omgadd  10979  ccatval1  11086  ccatval2  11087  ccatval3  11088  ccatass  11097  ccats1val2  11125  swrdval2  11137  swrdlen  11138  pfxfv  11170  pfxnd  11175  pfxsuffeqwrdeq  11184  swrdswrdlem  11190  swrdswrd  11191  pfxswrd  11192  pfxpfx  11194  ccats1pfxeq  11200  ccats1pfxeqrex  11201  shftfibg  11216  elicc4abs  11490  xrmaxltsup  11654  xrmaxadd  11657  xrlemininf  11667  xrminltinf  11668  mulcn2  11708  fsumsplitsnun  11815  prodfrecap  11942  demoivreALT  12170  dvdsval2  12186  dvdsmodexp  12191  dvdsmulcr  12217  modmulconst  12219  dvdsexp  12257  oddge22np1  12277  modremain  12325  mulgcd  12422  mulgcdr  12424  gcddiv  12425  rpmulgcd  12432  rplpwr  12433  coprmdvds  12499  cncongr1  12510  dvdsnprmd  12532  prmexpb  12558  rpexp  12560  cncongrprm  12564  modprm0  12662  modprmn0modprm0  12664  coprimeprodsq  12665  pythagtriplem1  12673  pythagtriplem3  12675  pythagtriplem10  12677  pythagtriplem6  12678  pythagtriplem11  12682  pythagtriplem12  12683  pythagtriplem13  12684  pythagtriplem15  12686  pythagtriplem17  12688  pythagtriplem19  12690  pcdvdsb  12728  dvdsprmpweqle  12745  pcfaclem  12757  isstructr  12932  setsvala  12948  setsresg  12955  strle3g  13025  imasaddvallemg  13232  fvprif  13260  mgmsscl  13278  insubm  13402  dfgrp3mlem  13515  mulgdirlem  13574  mulgp1  13576  mulgmodid  13582  eqglact  13646  rngdi  13787  rngdir  13788  rmodislmodlem  14197  rmodislmod  14198  lssclg  14211  2idlcpblrng  14370  qusmulrng  14379  clsss  14675  ntrcls0  14688  neiss  14707  neipsm  14711  cnpnei  14776  cncnp2m  14788  cnconst2  14790  sslm  14804  upxp  14829  txmetcn  15076  ptolemy  15381  sincosq1eq  15396  rplogbval  15502  rpcxplogb  15521  lgsdirprm  15596  lgsdirnn0  15609  gausslemma2dlem1a  15620  gausslemma2dlem3  15625  2lgslem1a1  15648  2lgsoddprmlem1  15667  2lgsoddprmlem2  15668  structiedg0val  15724  lpvtx  15760  incistruhgr  15771  upgredg2vtx  15822  upgredgpr  15823  findset  16050