Theorem 3ad2ant3 987

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 273	. 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜒)
3	2	3adant1 982	1 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 945

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 947

This theorem is referenced by:  simp3l  992  simp3r  993  simp31  1000  simp32  1001  simp33  1002  simp3ll  1035  simp3lr  1036  simp3rl  1037  simp3rr  1038  simp3l1  1069  simp3l2  1070  simp3l3  1071  simp3r1  1072  simp3r2  1073  simp3r3  1074  simp31l  1087  simp31r  1088  simp32l  1089  simp32r  1090  simp33l  1091  simp33r  1092  simp311  1111  simp312  1112  simp313  1113  simp321  1114  simp322  1115  simp323  1116  simp331  1117  simp332  1118  simp333  1119  3anim123i  1149  3jaao  1269  ceqsalt  2683  ceqsralt  2684  vtoclgft  2707  ifbothdc  3470  tpssi  3652  sotricim  4205  elirr  4416  en2lp  4429  reg3exmidlemwe  4453  sotri2  4894  poltletr  4897  funprg  5131  funtpg  5132  fntpg  5137  funimaexglem  5164  fvun1  5441  ftpg  5558  fsnunf  5574  fsnunfv  5575  caovimo  5918  brtposg  6105  smoel  6151  rdgivallem  6232  frecsuclem  6257  mapxpen  6695  unsnfi  6760  unsnfidcex  6761  unsnfidcel  6762  sbthlemi4  6800  elfir  6813  updjud  6919  ltsopi  7076  distrnqg  7143  ltmnqg  7157  mulcanenq0ec  7201  distrnq0  7215  prarloclem5  7256  1idprl  7346  1idpru  7347  ltaprg  7375  recexprlemopl  7381  recexprlemopu  7383  recexprlem1ssl  7389  aptipr  7397  ltmprr  7398  cauappcvgprlemlol  7403  cauappcvgprlemupu  7405  caucvgprlemlol  7426  caucvgprlemupu  7428  caucvgprprlemlol  7454  caucvgprprlemupu  7456  readdcan  7825  cnegexlem2  7861  addcan2  7866  ltadd2  8100  apreap  8267  ltmul1  8272  apcotr  8287  apadd1  8288  mulext1  8292  divdirap  8370  divcanap5  8387  ltdiv1  8536  lt2halves  8859  zdivmul  9045  eluzsub  9257  ledivge1le  9412  addlelt  9448  xaddass  9545  xleadd1  9551  xltadd1  9552  elioo5  9609  iccsupr  9642  iccneg  9665  icoshft  9666  icoshftf1o  9667  zltaddlt1le  9682  fzen  9716  elfz1b  9763  fzrevral  9778  fzshftral  9781  elfz0ubfz0  9795  elfz0fzfz0  9796  fz0fzelfz0  9797  fz0fzdiffz0  9800  elfzo  9819  fzodcel  9822  elfzonlteqm1  9880  modqaddmulmod  10057  expdivap  10237  leexp2a  10239  bcval3  10390  omgadd  10441  shftfibg  10485  elicc4abs  10758  xrmaxltsup  10919  xrmaxadd  10922  xrlemininf  10932  xrminltinf  10933  mulcn2  10973  fsumsplitsnun  11080  demoivreALT  11330  dvdsval2  11344  dvdsmulcr  11371  modmulconst  11373  dvdsexp  11407  oddge22np1  11426  modremain  11474  mulgcd  11550  mulgcdr  11552  gcddiv  11553  rpmulgcd  11560  rplpwr  11561  coprmdvds  11619  cncongr1  11630  dvdsnprmd  11652  prmexpb  11675  rpexp  11677  cncongrprm  11681  isstructr  11817  setsvala  11833  setsresg  11840  strle3g  11894  clsss  12130  ntrcls0  12143  neiss  12162  neipsm  12166  cnpnei  12230  cncnp2m  12242  cnconst2  12244  sslm  12258  upxp  12283  txmetcn  12508  findset  12835