Theorem 3adantl3 1148

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

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  dif1en  8548  infpssrlem4  9528  fin23lem11  9539  tskwun  10006  gruf  10033  lediv2a  11337  prunioo  12686  nn0p1elfzo  12898  hashunsnggt  13571  rpnnen2lem7  15436  muldvds1  15497  muldvds2  15498  dvdscmul  15499  dvdsmulc  15500  rpexp  15923  pospropd  17605  mdetmul  20939  elcls  21388  iscnp4  21578  cnpnei  21579  cnpflf2  22315  cnpflf  22316  cnpfcf  22356  xbln0  22730  blcls  22822  iimulcl  23247  icccvx  23260  iscau2  23586  rrxcph  23701  cncombf  23965  mumul  25463  ax5seglem1  26420  ax5seglem2  26421  clwwlkinwwlk  27558  clwwlkinwwlkOLD  27559  nvmul0or  28207  fh1  29179  fh2  29180  cm2j  29181  pjoi0  29278  hoadddi  29364  hmopco  29584  padct  30210  iocinif  30259  volfiniune  31134  eulerpartlemb  31271  ivthALT  33204  lindsadd  34326  cnambfre  34381  rngohomco  34694  rngoisoco  34702  pexmidlem3N  36553  hdmapglem7  38510  relexpmulg  39418  supxrgere  41031  supxrgelem  41035  supxrge  41036  infxr  41065  infleinflem2  41069  rexabslelem  41124  lptre2pt  41353  fnlimfvre  41387  limsupmnfuzlem  41439  climisp  41459  limsupgtlem  41490  dvnprodlem1  41662  ibliccsinexp  41667  iblioosinexp  41669  fourierdlem12  41836  fourierdlem41  41865  fourierdlem42  41866  fourierdlem48  41871  fourierdlem49  41872  fourierdlem51  41874  fourierdlem73  41896  fourierdlem74  41897  fourierdlem75  41898  fourierdlem97  41920  etransclem24  41975  ioorrnopnlem  42021  issalnnd  42060  sge0rpcpnf  42135  sge0seq  42160  meaiuninc3v  42198  smfmullem4  42501  smflimsupmpt  42535  smfliminfmpt  42538  lincdifsn  43847