Theorem 3adantl3 1185

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  dif1ennnALT  9236  infpssrlem4  10289  fin23lem11  10300  tskwun  10768  gruf  10795  lediv2a  12108  prunioo  13507  nn0p1elfzo  13730  hashunsnggt  14429  rpnnen2lem7  16275  muldvds1  16337  muldvds2  16338  dvdscmul  16339  dvdsmulc  16340  rpexp  16780  pospropd  18380  mdetmul  22748  elcls  23198  iscnp4  23388  cnpnei  23389  cnpflf2  24125  cnpflf  24126  cnpfcf  24166  xbln0  24539  blcls  24631  iimulcl  25064  icccvx  25077  iscau2  25404  rrxcph  25519  cncombf  25785  mumul  27310  noetalem1  27870  ax5seglem1  29218  ax5seglem2  29219  wwlksnext  30182  clwwlkinwwlk  30331  nvmul0or  30942  fh1  31910  fh2  31911  cm2j  31912  pjoi0  32009  hoadddi  32095  hmopco  32315  padct  33003  iocinif  33066  volfiniune  34564  eulerpartlemb  34702  ivthALT  36734  axtcond  36877  lindsadd  38151  cnambfre  38206  rngohomco  38512  rngoisoco  38520  pexmidlem3N  40635  hdmapglem7  42592  sticksstones12a  42813  relexpmulg  44327  supxrgere  45940  supxrgelem  45944  supxrge  45945  infxr  45973  infleinflem2  45977  rexabslelem  46023  pimxrneun  46093  lptre2pt  46245  fnlimfvre  46279  limsupmnfuzlem  46331  climisp  46351  limsupgtlem  46382  dvnprodlem1  46551  ibliccsinexp  46556  iblioosinexp  46558  fourierdlem12  46724  fourierdlem41  46753  fourierdlem42  46754  fourierdlem48  46759  fourierdlem49  46760  fourierdlem51  46762  fourierdlem73  46784  fourierdlem74  46785  fourierdlem75  46786  fourierdlem97  46808  etransclem24  46863  ioorrnopnlem  46909  issalnnd  46950  sge0rpcpnf  47026  sge0seq  47051  meaiuninc3v  47089  smfmullem4  47399  smflimsupmpt  47434  smfliminfmpt  47437  lincdifsn  49088  uptrlem1  49872