Theorem 3ad2ant3 1022

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  simp3l  1027  simp3r  1028  simp31  1035  simp32  1036  simp33  1037  simp3ll  1070  simp3lr  1071  simp3rl  1072  simp3rr  1073  simp3l1  1104  simp3l2  1105  simp3l3  1106  simp3r1  1107  simp3r2  1108  simp3r3  1109  simp31l  1122  simp31r  1123  simp32l  1124  simp32r  1125  simp33l  1126  simp33r  1127  simp311  1146  simp312  1147  simp313  1148  simp321  1149  simp322  1150  simp323  1151  simp331  1152  simp332  1153  simp333  1154  3anim123i  1186  3jaao  1319  ceqsalt  2778  ceqsralt  2779  vtoclgft  2802  ifbothdc  3582  tpssi  3774  sotricim  4341  elirr  4558  en2lp  4571  reg3exmidlemwe  4596  sotri2  5044  poltletr  5047  funprg  5285  funtpg  5286  fntpg  5291  funimaexglem  5318  fvun1  5603  ftpg  5721  fsnunf  5737  fsnunfv  5738  caovimo  6090  brtposg  6279  smoel  6325  rdgivallem  6406  frecsuclem  6431  mapxpen  6876  unsnfi  6947  unsnfidcex  6948  unsnfidcel  6949  sbthlemi4  6989  elfir  7002  updjud  7111  ltsopi  7349  distrnqg  7416  ltmnqg  7430  mulcanenq0ec  7474  distrnq0  7488  prarloclem5  7529  1idprl  7619  1idpru  7620  ltaprg  7648  recexprlemopl  7654  recexprlemopu  7656  recexprlem1ssl  7662  aptipr  7670  ltmprr  7671  cauappcvgprlemlol  7676  cauappcvgprlemupu  7678  caucvgprlemlol  7699  caucvgprlemupu  7701  caucvgprprlemlol  7727  caucvgprprlemupu  7729  readdcan  8127  cnegexlem2  8163  addcan2  8168  ltadd2  8406  apreap  8574  ltmul1  8579  apcotr  8594  apadd1  8595  mulext1  8599  divdirap  8684  divcanap5  8701  ltdiv1  8855  lt2halves  9184  zdivmul  9373  eluzsub  9587  ledivge1le  9756  addlelt  9798  xaddass  9899  xleadd1  9905  xltadd1  9906  elioo5  9963  iccsupr  9996  iccneg  10019  icoshft  10020  icoshftf1o  10021  zltaddlt1le  10037  fzen  10073  elfz1b  10120  fzrevral  10135  fzshftral  10138  elfz0ubfz0  10155  elfz0fzfz0  10156  fz0fzelfz0  10157  fz0fzdiffz0  10160  elfzo  10179  fzodcel  10182  elfzonlteqm1  10240  modqaddmulmod  10422  expdivap  10602  leexp2a  10604  bcval3  10763  omgadd  10814  shftfibg  10861  elicc4abs  11135  xrmaxltsup  11298  xrmaxadd  11301  xrlemininf  11311  xrminltinf  11312  mulcn2  11352  fsumsplitsnun  11459  prodfrecap  11586  demoivreALT  11813  dvdsval2  11829  dvdsmodexp  11834  dvdsmulcr  11860  modmulconst  11862  dvdsexp  11899  oddge22np1  11918  modremain  11966  mulgcd  12049  mulgcdr  12051  gcddiv  12052  rpmulgcd  12059  rplpwr  12060  coprmdvds  12124  cncongr1  12135  dvdsnprmd  12157  prmexpb  12183  rpexp  12185  cncongrprm  12189  modprm0  12286  modprmn0modprm0  12288  coprimeprodsq  12289  pythagtriplem1  12297  pythagtriplem3  12299  pythagtriplem10  12301  pythagtriplem6  12302  pythagtriplem11  12306  pythagtriplem12  12307  pythagtriplem13  12308  pythagtriplem15  12310  pythagtriplem17  12312  pythagtriplem19  12314  pcdvdsb  12352  dvdsprmpweqle  12369  pcfaclem  12381  isstructr  12527  setsvala  12543  setsresg  12550  strle3g  12620  imasaddvallemg  12792  fvprif  12819  mgmsscl  12837  insubm  12937  dfgrp3mlem  13042  mulgdirlem  13093  mulgp1  13095  mulgmodid  13101  eqglact  13164  rngdi  13294  rngdir  13295  rmodislmodlem  13666  rmodislmod  13667  lssclg  13680  2idlcpblrng  13838  qusmulrng  13846  clsss  14075  ntrcls0  14088  neiss  14107  neipsm  14111  cnpnei  14176  cncnp2m  14188  cnconst2  14190  sslm  14204  upxp  14229  txmetcn  14476  ptolemy  14702  sincosq1eq  14717  rplogbval  14820  rpcxplogb  14839  lgsdirprm  14893  lgsdirnn0  14906  2lgsoddprmlem1  14911  2lgsoddprmlem2  14912  findset  15155