Theorem 3adantl3 1170

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  dif1ennnALT  9187  infpssrlem4  10228  fin23lem11  10239  tskwun  10707  gruf  10734  lediv2a  12050  prunioo  13434  nn0p1elfzo  13657  hashunsnggt  14356  rpnnen2lem7  16187  muldvds1  16249  muldvds2  16250  dvdscmul  16251  dvdsmulc  16252  rpexp  16692  pospropd  18291  mdetmul  22588  elcls  23038  iscnp4  23228  cnpnei  23229  cnpflf2  23965  cnpflf  23966  cnpfcf  24006  xbln0  24379  blcls  24471  iimulcl  24904  icccvx  24917  iscau2  25244  rrxcph  25359  cncombf  25625  mumul  27144  noetalem1  27705  ax5seglem1  28997  ax5seglem2  28998  wwlksnext  29961  clwwlkinwwlk  30110  nvmul0or  30721  fh1  31689  fh2  31690  cm2j  31691  pjoi0  31788  hoadddi  31874  hmopco  32094  padct  32791  iocinif  32854  volfiniune  34374  eulerpartlemb  34512  ivthALT  36517  axtcond  36660  lindsadd  37934  cnambfre  37989  rngohomco  38295  rngoisoco  38303  pexmidlem3N  40418  hdmapglem7  42375  sticksstones12a  42596  relexpmulg  44137  supxrgere  45763  supxrgelem  45767  supxrge  45768  infxr  45796  infleinflem2  45800  rexabslelem  45846  pimxrneun  45916  lptre2pt  46068  fnlimfvre  46102  limsupmnfuzlem  46154  climisp  46174  limsupgtlem  46205  dvnprodlem1  46374  ibliccsinexp  46379  iblioosinexp  46381  fourierdlem12  46547  fourierdlem41  46576  fourierdlem42  46577  fourierdlem48  46582  fourierdlem49  46583  fourierdlem51  46585  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem97  46631  etransclem24  46686  ioorrnopnlem  46732  issalnnd  46773  sge0rpcpnf  46849  sge0seq  46874  meaiuninc3v  46912  smfmullem4  47222  smflimsupmpt  47257  smfliminfmpt  47260  lincdifsn  48900  uptrlem1  49685