Theorem 3adantl3 1187

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)

Hypothesis

Ref	Expression
3adantl.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adantl3	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Proof of Theorem 3adantl3

Step	Hyp	Ref	Expression
1		3simpa 1166	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜏) → (𝜑 ∧ 𝜓))
2		3adantl.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylan 592	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  dif1ennnALT  9247  infpssrlem4  10308  fin23lem11  10319  tskwun  10793  gruf  10820  lediv2a  12133  prunioo  13534  nn0p1elfzo  13758  hashunsnggt  14458  rpnnen2lem7  16308  muldvds1  16370  muldvds2  16371  dvdscmul  16372  dvdsmulc  16373  rpexp  16813  pospropd  18413  mdetmul  22845  elcls  23298  iscnp4  23488  cnpnei  23489  cnpflf2  24226  cnpflf  24227  cnpfcf  24267  xbln0  24640  blcls  24732  iimulcl  25165  icccvx  25178  iscau2  25505  rrxcph  25620  cncombf  25886  mumul  27417  noetalem1  27977  ax5seglem1  29385  ax5seglem2  29386  wwlksnext  30361  clwwlkinwwlk  30510  nvmul0or  31131  fh1  32099  fh2  32100  cm2j  32101  pjoi0  32198  hoadddi  32284  hmopco  32504  padct  33189  iocinif  33252  volfiniune  34741  eulerpartlemb  34879  ivthALT  36954  axtcond  37097  lindsadd  38367  cnambfre  38417  rngohomco  38724  rngoisoco  38732  pexmidlem3N  40845  hdmapglem7  42802  sticksstones12a  43023  relexpmulg  44550  supxrgere  46163  supxrgelem  46167  supxrge  46168  infxr  46196  infleinflem2  46200  rexabslelem  46246  pimxrneun  46316  lptre2pt  46468  fnlimfvre  46502  limsupmnfuzlem  46554  climisp  46574  limsupgtlem  46605  dvnprodlem1  46774  ibliccsinexp  46779  iblioosinexp  46781  fourierdlem12  46947  fourierdlem41  46976  fourierdlem42  46977  fourierdlem48  46982  fourierdlem49  46983  fourierdlem51  46985  fourierdlem73  47007  fourierdlem74  47008  fourierdlem75  47009  fourierdlem97  47031  etransclem24  47086  ioorrnopnlem  47132  issalnnd  47173  sge0rpcpnf  47249  sge0seq  47274  meaiuninc3v  47312  smfmullem4  47622  smflimsupmpt  47657  smfliminfmpt  47660  lincdifsn  49354  uptrlem1  50136