Theorem 3adantl3 1212

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 1051	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜏) → (𝜑 ∧ 𝜓))
2		3adantl.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylan 487	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033

This theorem is referenced by:  dif1en  8078  infpssrlem4  9011  fin23lem11  9022  tskwun  9485  gruf  9512  lediv2a  10796  prunioo  12172  nn0p1elfzo  12378  rpnnen2lem7  14788  muldvds1  14844  muldvds2  14845  dvdscmul  14846  dvdsmulc  14847  rpexp  15270  pospropd  16957  mdetmul  20248  elcls  20687  iscnp4  20877  cnpnei  20878  cnpflf2  21614  cnpflf  21615  cnpfcf  21655  xbln0  22029  blcls  22121  iimulcl  22544  icccvx  22557  iscau2  22883  rrxcph  22988  cncombf  23231  mumul  24707  ax5seglem1  25608  ax5seglem2  25609  wwlkext2clwwlk  26331  nvmul0or  26889  fh1  27861  fh2  27862  cm2j  27863  pjoi0  27960  hoadddi  28046  hmopco  28266  padct  28885  iocinif  28933  volfiniune  29620  eulerpartlemb  29757  ivthALT  31500  cnambfre  32628  rngohomco  32943  rngoisoco  32951  pexmidlem3N  34276  hdmapglem7  36239  relexpmulg  37021  supxrgere  38490  supxrgelem  38494  supxrge  38495  infxr  38524  infleinflem2  38528  lptre2pt  38707  fnlimfvre  38741  dvnprodlem1  38836  ibliccsinexp  38842  iblioosinexp  38844  fourierdlem12  39012  fourierdlem41  39041  fourierdlem42  39042  fourierdlem48  39047  fourierdlem49  39048  fourierdlem51  39050  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem97  39096  etransclem24  39151  ioorrnopnlem  39200  issalnnd  39239  sge0rpcpnf  39314  sge0seq  39339  smfmullem4  39679  wwlksext2clwwlk  41231  lincdifsn  42007